Opened 3 years ago
Last modified 3 years ago
#11207 new bug
GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on userdefined Nat kind
Reported by:  duairc  Owned by:  

Priority:  normal  Milestone:  
Component:  Compiler (Type checker)  Version:  7.11 
Keywords:  TypeFamilies  Cc:  jstolarek 
Operating System:  Unknown/Multiple  Architecture:  Unknown/Multiple 
Type of failure:  None/Unknown  Test Case:  
Blocked By:  Blocking:  
Related Tickets:  Differential Rev(s):  
Wiki Page: 
Description
The following does not work:
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #} import GHC.TypeLits (Nat, type ()) type family Replicate (n :: Nat) (a :: k) = (r :: [k])  r > n where Replicate 0 a = '[] Replicate n a = a ': Replicate (n  1) a
It fails to compile with the following error:
error: • Type family equation violates injectivity annotation. Type variable ‘n’ cannot be inferred from the righthand side. In the type family equation: forall (k :: BOX) (n :: Nat) (a :: k). Replicate n a = a : Replicate (n  1) a • In the equations for closed type family ‘Replicate’ In the type family declaration for ‘Replicate’ Failed, modules loaded: none.
However, the following does:
{# LANGUAGE DataKinds, PolyKinds, TypeFamilies, TypeOperators, UndecidableInstances #} data Nat = Zero  Succ Nat type family Replicate (n :: Nat) (a :: k) = (r :: [k])  r > n where Replicate Zero a = '[] Replicate (Succ n) a = a ': Replicate n a
Sure GHC.TypeLits' builtin Nat type is isomorphic to the one defined above, and thus GHC should be able to infer injectivity for Replicate?
Change History (9)
comment:1 Changed 3 years ago by
Version:  7.10.2 → 7.11 

comment:2 Changed 3 years ago by
Cc:  jstolarek added 

comment:3 Changed 3 years ago by
You're right, they are subtley different. But I can't "patternmatch" on (n + 1) on the LHS with GHC's TypeLits, because + is a type family and not a constructor. If there was some other way I could accomplish this then I would be satisfied with that for now. But obviously if we could get generalised injectivity that we be awesome.
comment:4 Changed 3 years ago by
You're absolutely right  there is no way to fix the TypeLits
style, until we have generalized injectivity.
comment:5 Changed 3 years ago by
Could it not be possible to introduce some way of patternmatching on GHC.TypeLits
's Nat
s independently of generalised injectivity? Maybe it's a question that would involve a lot of bikeshedding... but surely the compiler ultimately has enough information to prove that Replicate
is injective, I just can't destructure typelevel Nat
s. Could there be a magic builtin pattern synonym Succ
for Nat
s? Can pattern synonyms work on the type level? I don't really know much about the internals to know how to implement that, but there must be a way.
Like if full generalised injectivity is just around the corner, then maybe we should just wait for that, but from what I've read it sounds like there are still a lot of kinks that need to be worked out first and it might turn out to be too difficult altogether? Right now pretty much every package that does typelevel stuff defines its own Nat
type, and I'd imagine the lack of the ability to pattern match on GHC.TypeLits
's Nat
is a big part of the reason for that.
comment:6 followup: 7 Changed 3 years ago by
Typelevel pattern synonyms would be great. But no one is working on that, I'm afraid. The way that type patterns are implemented now would make this difficult, but I'm planning on refactoring it in the near future (next month, probably). Once that is done, I don't imagine it would be hard to have typelevel pattern synonyms. And then we might be able to provide the patternmatching on TypeLits
that we all want.
I do think that generalized injectivity is the fastest way toward what you want, though.
comment:7 Changed 3 years ago by
Replying to goldfire:
I do think that generalized injectivity is the fastest way toward what you want, though.
Note however, that generalized injectivity will not make it into 8.0 (unless miracle happens), which means over a year of waiting until it makes it into next stable release.
comment:8 Changed 3 years ago by
Component:  Compiler → Compiler (Type checker) 

comment:9 Changed 3 years ago by
Keywords:  TypeFamilies added 

But your definitions are subtly different. In the TypeLits case, you're using

in the RHS.
is not injective. So GHC quite correctly rejects the equation. In the corresponding equation without TypeLits, there are no function calls on the right; instead, you use patternmatching on the left to get what you want.If you implement a

over your unaryNat
and write the definitions the same way, GHC will reject the nonTypeLits definition, too.What this requires is "generalized injectivity", where we could say
We've considered such a thing, but we have yet to work out all the details, if I recall correctly. In any case, if this existed, then GHC would be able to accept the first definition.
Adding in Janek, who is Mr. InjectiveTypeFamilies.