Kind error with type equality
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)
Trac metadata
Trac field | Value |
---|---|
Version | 8.0.1 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler (Type checker) |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | goldfire |
Operating system | |
Architecture |