## #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 22 months ago by

### comment:2 Changed 22 months ago by

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 22 months ago by

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'`

.

### comment:4 Changed 22 months ago by

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 follow-up: 7 Changed 22 months ago by

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 22 months ago by

Resolution: | → invalid |
---|---|

Status: | new → closed |

### comment:7 Changed 22 months ago by

Replying to int-index:

Ok, so if I write

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

`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 22 months ago by

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.

I agree with GHC here.

The problem is that

`UnT`

takes`k`

as a parameter. It doesnotlook 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:Please close the ticket if you agree with my analysis. Thanks!