Can't create injective type family equation with TypeError as the RHS
For the longest time, I've wanted to make a type family like this injective:
type family Foo (a :: *) :: * where
Foo Bar = Int
Foo Baz = Char
But the problem is that Foo
is defined on //all// types of kind *
, so the above definition is inherently non-injective. With the introduction of TypeError
s, however, I thought I could rule out all other cases:
import GHC.TypeLits
type family Foo (a :: *) = (r :: *) | r -> a where
Foo Bar = Int
Foo Baz = Char
Foo _ = TypeError ('Text "boom")
But this doesn't work, sadly:
Injective.hs:18:3: error:
• Type family equations violate injectivity annotation:
Foo Bar = Int -- Defined at Injective.hs:18:3
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
Injective.hs:20:3: error:
• Type family equation violates injectivity annotation.
Type variable ‘_’ cannot be inferred from the right-hand side.
In the type family equation:
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
Injective.hs:20:3: error:
• Type family equation violates injectivity annotation.
RHS of injective type family equation cannot be a type family:
Foo _ = (TypeError ...) -- Defined at Injective.hs:20:3
• In the equations for closed type family ‘Foo’
In the type family declaration for ‘Foo’
From GHC's perspective, TypeError
is just another type family, so it thinks it violates injectivity. But should this be the case? After all, having the RHS of a type family equation being TypeError
is, in my perspective, tantamount to making that type family undefined for those inputs. It seems like if we successfully conclude that Foo a ~ Foo b
(and GHC hasn't blown up yet due to type erroring), we should be able to conclude that a ~ b
.
Could this be accomplished by simply adding a special case for TypeError
in the injectivity checker?
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | FeatureRequest |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire, jstolarek |
Operating system | |
Architecture |