GHC forgets constraints when matching on GADTs
Here's a relatively short piece of code that doesn't compile:
{-# LANGUAGE MultiParamTypeClasses, TypeFamilies, GADTs,
ConstraintKinds, KindSignatures,
FlexibleInstances #-}
module Foo where
import GHC.Exts
data Foo m zp r'q = Foo zp
data Dict :: Constraint -> * where
Dict :: a => Dict a
type family BarFamily a b :: Bool
class Bar m m'
instance (BarFamily m m' ~ 'True) => Bar m m'
magic :: (Bar m m') => c m zp -> Foo m zp (c m' zq)
magic = undefined
getDict :: a -> Dict (Num a)
getDict _ = undefined
fromScalar :: r -> c m r
fromScalar = undefined
foo :: (Bar m m')
=> c m zp -> Foo m zp (c m' zq) -> Foo m zp (c m' zq)
foo b (Foo sc) =
let scinv = fromScalar sc
in case getDict scinv of
Dict -> magic $ scinv * b
GHC complains that it cannot deduce (BarFamily m m' ~ 'True) arising from a use of
magic
in the definition of foo
. Of course this is silly: magic
requires Bar m m'
, which is supplied as a constraint to foo
. So GHC is forgetting about the constraint on foo
and instead trying to satisfy the generic instance of Bar
which has the constraint (BarFamily m m' ~ 'True)
.
I've found no less than six different ways to poke this code to make it compile, and some of them seem to reveal dangerous/unexpected behavior. The following are all deltas from the original code above and result in compiling code.
- Add
ScopedTypeVariables
and givescinv
an explicit signature:
let scinv = fromScalar sc :: c m z in ...
I'm not sure why this would make GHC suddenly realize that it already has the constraint Bar m m'
, but it seems to. (What it definitely does *not* do is result in a BarFamily m m' ~ 'True
constraint.)
- Remove the instance for
Bar
.
This seems highly suspicious: the presence (or lack thereof) of an instance changes how GHC resolves the constraint in foo
.
- Change the constraint on
foo
toBarFamily m m' ~ 'True
. In this case, GHC does *not* forget the constraint onfoo
and successfully uses it to satisfy the instance ofBar
. Why does GHC forget aboutBar m m'
but notBarFamily m m' ~ 'True
? - Add the superclass constraint
BarFamily m m' ~ 'True
to classBar
. Adding this constraint either makes GHC find theBar m m'
constraint onfoo
or, even more bizarrely, GHC still forgets aboutBar m m'
but manages to get the superclass constraint fromBar m m'
and uses it to satisfy the instance. - Add
PolyKinds
. Not sure why this would affect anything. - Change the signature of
fromScalar
tor -> s
. Not sure why this would affect anything.