CODEWITHSUNDEEP
haskelltype-families
Alexey Vagarenko
Alexey Vagarenko

Reputation: 1196

Is this type family injective?

I have type family for N-ary function from n arguments of type t to value of type o:

type family NAry (n :: Nat) (t :: Type) (o :: Type) = (r :: Type) | r -> n t o where
    NAry 1 t o = t -> o
    NAry n t o = t -> (NAry (n - 1) t o)

I think this family ought to be injective by I can't prove it to GHC:

error:
    * Type family equations violate injectivity annotation:
        NAry 1 t o = t -> o
        NAry n t o = t -> NAry (n - 1) t o
error:
    * Type family equation violates injectivity annotation.
      Type variable `n' cannot be inferred from the right-hand side.
      In the type family equation:
        NAry n t o = t -> NAry (n - 1) t o

Upvotes: 1

Views: 210

Answers (1)

Daniel Wagner
Daniel Wagner

Reputation: 152837

It's not as injective as you promise. Take the type

Int -> Int -> Bool

and ask: is this NAry 2 Int Bool or NAry 1 Int (Int -> Bool)?

Upvotes: 10

Related Questions