Opened 8 months ago

Closed 8 months ago

Last modified 8 months ago

#13546 closed bug (invalid)

Kind error with type equality

Reported by: int-index Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 8.0.1
Keywords: TypeInType Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

This code

{-# LANGUAGE TypeInType, TypeFamilies, GADTs, ConstraintKinds #-}

import Data.Kind

data Dict c where
  Dict :: c => Dict c

data T (t :: k)

type family UnT (a :: Type) :: k where
  UnT (T t) = t

untt :: Dict (UnT (T "a") ~ "a")
untt = Dict

tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict

fails with this error:

tunt.hs:17:8: error:
    • Couldn't match kind ‘k’ with ‘GHC.Types.Symbol’
      ‘k’ is a rigid type variable bound by
        the type signature for:
          tunt :: forall k. Dict T (UnT (T "a")) ~ T "a"
        at tunt.hs:16:1-38
      When matching types
        UnT (T "a") :: k
        "a" :: GHC.Types.Symbol
    • In the expression: Dict
      In an equation for ‘tunt’: tunt = Dict
    • Relevant bindings include
        tunt :: Dict T (UnT (T "a")) ~ T "a" (bound at tunt.hs:17:1)
   |
17 | tunt = Dict
   | 

Instead I would expect these reductions to take place:

 1. T (UnT (T "a")) ~ T "a"
 2. T "a" ~ T "a"
 3. constraint satisfied (refl)

Change History (8)

comment:1 Changed 8 months ago by goldfire

I agree with GHC here.

The problem is that UnT takes k as a parameter. It does not look at the kind at which its argument is used and return something of that kind.

So, in the type of tunt, the first T is applied at an unknown kind, which is also the return kind of UnT. Of course, you want this to be Symbol, but GHC doesn't know this. Adding a kind signature fixes the problem:

tunt :: Dict (T (UnT (T "a") :: Symbol) ~ T "a")
tunt = Dict

Please close the ticket if you agree with my analysis. Thanks!

comment:2 Changed 8 months ago by goldfire

It's possible you want this behavior, though, which avoids the need for the kind signature:

type family UnTKind (a :: Type) :: Type where
  UnTKind (T (_ :: k)) = k

type family UnT (a :: Type) :: UnTKind a where
  UnT (T t) = t

tunt :: Dict (T (UnT (T "a")) ~ T "a")
tunt = Dict

comment:3 Changed 8 months ago by int-index

I did not realize that k is a parameter, now the error is clear to me. However, then the definition of UnT should be rejected, no?

type family UnT (a :: Type) :: k where
  UnT (T (t :: k')) = t

UnT has kind forall k. Type -> k, but in the clause UnT (T t) = t it returns something of the kind k'. There's no guarantee that k ~ k'.

Last edited 8 months ago by int-index (previous) (diff)

comment:4 Changed 8 months ago by goldfire

Not quite. UnT really has kind pi k. Type -> k, because the k can be used in pattern-matching. The behavior of UnT is to reduce only when the (invisibly) provided k matches the kind of the argument of T. Unlike when defining ordinary functions, polymorphism in type families is not parametric.

comment:5 Changed 8 months ago by int-index

Ok, so if I write

type family UnT (a :: Type) :: k where
  UnT (T (t :: k')) = t

the k ~ k' proof for the RHS is provided by the LHS.

Can I write a LHS that will match on t :: k' for all kinds k' and try to unify k ~ k' only on the RHS?

comment:6 Changed 8 months ago by int-index

Resolution: invalid
Status: newclosed

comment:7 in reply to:  5 Changed 8 months ago by goldfire

Replying to int-index:

Ok, so if I write

type family UnT (a :: Type) :: k where
  UnT (T (t :: k')) = t

the k ~ k' proof for the RHS is provided by the LHS.

Roughly, yes. That instance (with kinds written explicitly) becomes UnT k' (T k' t) = t. So the pattern-matcher needs both kinds to be the same.

Can I write a LHS that will match on t :: k' for all kinds k' and try to unify k ~ k' only on the RHS?

I'm not sure what you mean here. Perhaps you're describing the type-family equivalent of the difference between

instance C a a

and

instance (a ~ b) => C a b

The former requires the two types to be the same, while the latter matches any types and then emits a constraint saying they're equal.

If I understand your question correctly, then: no. Type families don't support that right now. Perhaps in the future.

comment:8 Changed 8 months ago by int-index

Yes, the difference between C a a and a~b => C a b is what I meant. Thank you for explanations, very helpful!

Note: See TracTickets for help on using tickets.