Pattern matching in type families seemingly treats constructor constraints as wanted instead of as given
Summary
When pattern matching on a constructor that contains a constraint with a type family application (e.g. Not a ~ True => Foo a
) in a type family equation, GHC seemingly treats this constraint as wanted rather than as given, leading to a somewhat confusing error message.
Steps to reproduce
Load the following file into GHCi:
{-# LANGUAGE GADTs, TypeFamilies, DataKinds #-}
type family Not b where
Not True = False
Not False = True
data Foo a where MkFoo :: Not a ~ True => Foo a
data Bar a where MkBar :: Not a ~ True => Bar a
foo2bar :: Foo a -> Bar a
foo2bar MkFoo = MkBar
type Foo2Bar :: Foo a -> Bar a
type family Foo2Bar foo where
Foo2Bar MkFoo = MkBar
It produces the error
TyFamGADT.hs:15:11: error:
* Couldn't match expected kind 'True with actual kind `Not a'
* In the first argument of `Foo2Bar', namely `MkFoo'
In the type family declaration for `Foo2Bar'
|
15 | Foo2Bar MkFoo = MkBar
| ^^^^^
Note that interestingly, if I injectivity annotation is added (type family Not b = r | r -> b where
), the error message changes to the completely different
TyFamGADT.hs:15:3: error:
* Illegal type synonym family application `Not 'False' in instance:
Foo2Bar
@'False
('MkFoo @'False @{'GHC.Types.Eq# @Bool @(Not 'False) @'True <>})
* In the equations for closed type family `Foo2Bar'
In the type family declaration for `Foo2Bar'
|
15 | Foo2Bar MkFoo = MkBar
| ^^^^^^^^^^^^^^^^^^^^^
Expected behavior
Ideally, this should just work, just like the term-level function. Failing that, the error message could be improved, such that it doesn't look like the constraint is treated as a wanted constraint when you would expect it to be given.
Environment
- GHC version used: 9.6.2, 9.2.5
Optional:
- Operating System: Ubuntu on WSL on Windows 11
- System Architecture: x86_64