The following snippet makes GHC (checked with 8.6.2 & 8.4.4) stuck during compilation:
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE UndecidableSuperClasses #-}
import GHC.Exts (Constraint)
data T = T
type family F t (c :: * -> Constraint) :: Constraint
type instance F T c = c T
class F t C => C t where
t :: C T => t
t = undefined
I think that it gets stuck because for t
GHC tries to find C T
, which leads to F T C
which expands via type family F
back to C T
, which is what it was looking for (infinite loop).
I suppose that theoretically GHC could tell that it reached its quest for C T
from itself and that anything that depends on itself can work fine recursively, or am I misunderstanding something?
Side note: in the real example where I stumbled upon this behaviour I was able to achieve what I wanted without the compiler being stuck by replacing UndecidableSuperClasses
with Data.Constraint.Dict
instead.
UndecidableSuperClasses
does not make instance resolution lazy. The compiler will still expand superclass constraints as far as possible. I believe that the fields in instance dictionaries that point to the superclass dictionaries are strict, and GHC actually pins them down at compile time. This is in contrast to UndecidableInstances
, which allows instance constraints to be treated (a bit) lazily.
deriving instance Show (f (Fix f)) => Show (Fix f)
will work just fine. When resolving an instance for, e.g., Show (Fix Maybe)
), GHC will see that it needs Show (Maybe (Fix Maybe))
. It then sees it needs Show (Fix Maybe)
(which it's currently resolving) and accept that thanks to UndecidableInstances
.
All UndecidableSuperClases
does is disable the checks that guarantee that expansion won't loop. See the bit near the beginning of Ed Kmett's talk where he describes the process "reaching a fixed point".
Consider a working example (ripped from Data.Constraint.Forall
):
type family Skolem (p :: k -> Constraint) :: k
class p (Skolem p) => Forall (p :: k -> Constraint)
GHC only accepts this with UndecidableSuperclasses
. Why? Because it doesn't know anything about what that constraint might mean. As far as it knows, it could be the case that p (Skolem p)
will reduce to Forall p
. And that could actually happen!
class Forall P => P x
-- This definition loops the type checker
foo :: P x => x
foo = undefined