Type family equations with wrong name are accepted when the type family has a SAKS
Summary
Type family equations with wrong names are accepted when the type family has a standalone kind signature.
Steps to reproduce
{-# LANGUAGE TypeFamilies, StandaloneKindSignatures #-}
module Bug where
data Bar
type Foo :: *
type family Foo where
Bar = ()
Bar
used in equation is obviously wrong, still ghc compiles the program without an error. -ddump-types
reports correct axiom:
COERCION AXIOMS
axiom Bug.D:R:Foo :: Foo = ()
Expected behavior
I'd expect ghc to reject the program with the same error message it gives if Foo
had no SAKS
Bug.hs:7:3: error:
• Mismatched type name in type family instance.
Expected: Foo
Actual: Maybe
• In the type family declaration for ‘Foo’
|
7 | Maybe = ()
Environment
- GHC version used: 9.0.1, 9.3.20210819
Optional:
- Operating System: Linux (NixOS)
- System Architecture: x86-64