TypeFamilyDependencies aggressively requires UndecidableInstances on GHC HEAD
I originally noticed this as the singletons
library fails to compile with GHC HEAD. I will try to minimize the sources of breakage as much as possible. First, consider this module:
{-# LANGUAGE TypeFamilyDependencies #-}
module A where
data D a
type family F a = r | r -> a
type instance F (D a) = D (F a)
This compiles without issue on GHC 8.8.1 and earlier, but on HEAD it fails with:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 A.hs
[1 of 1] Compiling A ( A.hs, A.o )
A.hs:6:15: error:
Type family equation violates injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
Using UndecidableInstances might help
In the type family equation:
F (D a) = D (F a) -- Defined at A.hs:6:15
|
6 | type instance F (D a) = D (F a)
| ^
That's a strange error, as I would have expected F
's injectivity to be sufficient to determine what a
would be in that instance. That alone is probably enough to be considered a regression. Thankfully, that buglet is easy enough to work around: just add {-# LANGUAGE UndecidableInstances #-}
to A.hs
and it compiles again on HEAD.
However, things get even worse from here. Let's add two more modules into the mix:
{-# LANGUAGE TypeFamilyDependencies #-}
module B where
type family F2 a
type instance F2 Int = Bool
module C where
import A
import B
If I try to compile C
, I get a really baffling error:
$ ~/Software/ghc5/inplace/bin/ghc-stage2 --interactive C.hs
GHCi, version 8.9.0.20191023: https://www.haskell.org/ghc/ :? for help
Loaded GHCi configuration from /home/rgscott/.ghci
[1 of 3] Compiling A ( A.hs, interpreted )
[2 of 3] Compiling B ( B.hs, interpreted )
[3 of 3] Compiling C ( C.hs, interpreted )
A.hs:7:15: error:
Type family equation violates injectivity annotation.
Type variable ‘a’ cannot be inferred from the right-hand side.
Using UndecidableInstances might help
In the type family equation:
F (D a) = D (F a) -- Defined at A.hs:7:15
|
7 | type instance F (D a) = D (F a)
| ^
Failed, two modules loaded.
You're reading that right: when compiling C.hs
, I get an error message that points to a line of code in A.hs
. Wat. This definitely seems like a bug.
What's curious is that defining a type instance
in B.hs
appears to be essential to triggering this bug. If I comment out the type instance F2 Int = Bool
part, then compiling C.hs
works without a hitch.
Like before, you can work around the issue by adding {-# LANGUAGE UndecidableInstances #-}
to C.hs
. This is really cumbersome, however, because it effectively means one has to enable this language extension in every module that imports A
and another type family. In the particular case of the singletons
library, this translates to enabling UndecidableInstances
in almost every single module.
I'm almost positive this regression was introduced in 1cd3fa29, so cc'ing @rae.