Opened 2 years ago

Last modified 23 months ago

#11207 new bug

GHC cannot infer injectivity on type family operating on GHC.TypeLits' Nat, but can for equivalent type family operating on user-defined 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 right-hand 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' built-in 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 2 years ago by duairc

Version: 7.10.27.11

comment:2 Changed 2 years ago by goldfire

Cc: jstolarek 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 pattern-matching on the left to get what you want.

If you implement a - over your unary Nat and write the definitions the same way, GHC will reject the non-TypeLits definition, too.

What this requires is "generalized injectivity", where we could say

type family (a :: Nat) - (b :: Nat) = (r :: Nat) | r a -> b, r b -> a

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. Injective-Type-Families.

comment:3 Changed 2 years ago by duairc

You're right, they are subtley different. But I can't "pattern-match" 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 2 years ago by goldfire

You're absolutely right -- there is no way to fix the TypeLits style, until we have generalized injectivity.

comment:5 Changed 2 years ago by duairc

Could it not be possible to introduce some way of pattern-matching on GHC.TypeLits's Nats 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 type-level Nats. Could there be a magic built-in pattern synonym Succ for Nats? 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 type-level 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 Changed 2 years ago by goldfire

Type-level 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 type-level pattern synonyms. And then we might be able to provide the pattern-matching on TypeLits that we all want.

I do think that generalized injectivity is the fastest way toward what you want, though.

comment:7 in reply to:  6 Changed 2 years ago by jstolarek

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 23 months ago by thomie

Component: CompilerCompiler (Type checker)

comment:9 Changed 23 months ago by thomie

Keywords: TypeFamilies added
Note: See TracTickets for help on using tickets.