I'm playing around with a multikinded tagless encoding of Free
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeSynonymInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE Rank2Types #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE QuantifiedConstraints #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE TypeOperators #-}
module Free where
import GHC.Types
type (a :: k) ~> (b :: k) = Morphism k a b
newtype Natural (f :: j -> k) (g :: j -> k) =
Natural { getNatural :: forall (x :: j). f x ~> g x }
type family Morphism k :: k -> k -> Type where
Morphism Type = (->)
Morphism (j -> k) = Natural
class DataKind k where
data Free :: (k -> Constraint) -> k -> k
interpret :: forall (cls :: k -> Constraint) (u :: k) (v :: k).
cls v => (u ~> v) -> (Free cls u ~> v)
call :: forall (cls :: k -> Constraint) (u :: k).
u ~> Free cls u
instance DataKind Type where
newtype Free cls u = Free0
{ runFree0 :: forall v. cls v => (u ~> v) -> v }
interpret f = \(Free0 g) -> g f
call = \u -> Free0 $ \f -> f u
I can write Semigroup instances for Free Semigroup and Free Monoid without a problem:
instance Semigroup (Free Semigroup u) where
Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f
instance Semigroup (Free Monoid u) where
Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f
These instances are the same, and will be for any other subclass of Semigroup.
I want to use QuantifiedConstraints so I can just write one instance for all subclasses of Semigroup:
instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f
But the compiler (GHC-8.6.3) complains that it's unable to deduce cls (Free cls u):
Free.hs:57:10: error:
• Could not deduce: cls (Free cls u)
arising from a use of ‘GHC.Base.$dmsconcat’
from the context: forall v. cls v => Semigroup v
bound by the instance declaration at Free.hs:57:10-67
• In the expression: GHC.Base.$dmsconcat @(Free cls u)
In an equation for ‘GHC.Base.sconcat’:
GHC.Base.sconcat = GHC.Base.$dmsconcat @(Free cls u)
In the instance declaration for ‘Semigroup (Free cls u)’
• Relevant bindings include
sconcat :: GHC.Base.NonEmpty (Free cls u) -> Free cls u
(bound at Free.hs:57:10)
|
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Free.hs:57:10: error:
• Could not deduce: cls (Free cls u)
arising from a use of ‘GHC.Base.$dmstimes’
from the context: forall v. cls v => Semigroup v
bound by the instance declaration at Free.hs:57:10-67
or from: Integral b
bound by the type signature for:
GHC.Base.stimes :: forall b.
Integral b =>
b -> Free cls u -> Free cls u
at Free.hs:57:10-67
• In the expression: GHC.Base.$dmstimes @(Free cls u)
In an equation for ‘GHC.Base.stimes’:
GHC.Base.stimes = GHC.Base.$dmstimes @(Free cls u)
In the instance declaration for ‘Semigroup (Free cls u)’
• Relevant bindings include
stimes :: b -> Free cls u -> Free cls u (bound at Free.hs:57:10)
|
57 | instance (forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
When I add this as context for the instance, it compiles fine:
instance (cls (Free cls u), forall v. cls v => Semigroup v) => Semigroup (Free cls u) where
Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f
The added context is a little verbose, but since the whole point of Free is that cls (Free cls u) is always true, not onerous.
What I don't understand is why GHC needs to be able to conclude cls (Free cls u) for the subclass of Semigroup for the Semigroup instance to compile. I tried replacing the definition of (<>) with undefined and got the same error, so I think the issue is not in the implementation itself but in the declaration of the instance; probably due to some aspect of QuantifiedConstraints I don't understand.
The error messages state these errors come from the default definitions of sconcat and stimes. Quantified contexts act like instances: within your instance Semigroup (Free cls v), it's as if there is an instance cls v => Semigroup v in scope. instances are chosen by matching. sconcat and stimes want Semigroup (Free cls v), so they match that want against the context instance forall z. cls z => Semigroup z, succeed with z ~ Free cls v, and get a further wanted of cls (Free cls v). This happens even though we also have a recursive instance _etc => Semigroup (Free cls v) around. Remember, we assume that typeclass instances are coherent; there should be no difference whether the quantified context is used or the currently defined instance is used, so GHC just picks whichever instance it feels like using.
However, this is not a good situation. The quantified context overlaps with our instance (actually, it overlaps with every Semigroup instance), which is alarming. If you try something like (<>) = const (Free0 _etc) ([1, 2] <> [3, 4]), you get a similar error, because the quantified context overshadows the real instance Semigroup [a] in the library. I think including some ideas from issue 14877 can make this less uncomfortable:
class (a => b) => Implies a b
instance (a => b) => Implies a b
instance (forall v. cls v `Implies` Semigroup v) => Semigroup (Free cls u) where
Free0 g <> Free0 g' = Free0 $ \f -> g f <> g' f
Using Implies here means that the quantified context no longer matches the want for Semigroup (Free cls v) which is instead discharged by recursion. However, the requirement behind the constraint doesn't change. Essentially, we keep the requirement fragment of the quantified constraint, for the user, that Semigroup v should be implied by cls v, while slapping a safety on the discharge fragment, for the implementation, so it doesn't muck up our constraint resolution. The Implies constraint still can and has to be used to prove the Semigroup v constraint in (<>), but it's considered as a last resort after the explicit Semigroup instances are exhausted.