[GHC] #13546: Kind error with type equality
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 (Type checker) | Keywords: TypeInType | Operating System: Unknown/Multiple Architecture: | Type of failure: GHC rejects Unknown/Multiple | valid program Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- This code {{{#!hs {-# 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) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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: {{{#!hs tunt :: Dict (T (UnT (T "a") :: Symbol) ~ T "a") tunt = Dict }}} Please close the ticket if you agree with my analysis. Thanks! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): It's possible you want this behavior, though, which avoids the need for the kind signature: {{{#!hs 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 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): I did not realize that `k` is a parameter, now the error is clear to me. However, than the definition of `UnT` should be rejected, no? {{{#!hs 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'`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by int-index): Ok, so if I write {{{#!hs 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? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by int-index): * status: new => closed * resolution: => invalid -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Replying to [comment:5 int-index]:
Ok, so if I write
{{{#!hs 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#13546: Kind error with type equality -------------------------------------+------------------------------------- Reporter: int-index | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler (Type | Version: 8.0.1 checker) | Resolution: invalid | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (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! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13546#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC