[GHC] #14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N)
#14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- I was trying to create a pattern synonym that matches `TypeRep (a::k)` when `k ~ N`, witnessing the equality and returning the representation. This works fine: {{{#!hs {-# Language PatternSynonyms, ViewPatterns, GADTs, ConstraintKinds, RankNTypes, KindSignatures, PolyKinds, ScopedTypeVariables, DataKinds, TypeInType, TypeOperators, TypeApplications #-} import Type.Reflection import Data.Kind foo :: forall (kind::k') (a::k). TypeRep kind -> TypeRep a -> Maybe (kind :~~: k, TypeRep a) foo krep rep = do HRefl <- eqTypeRep krep (typeRepKind rep) pure (HRefl, rep) data N = O | S N pattern Bloop :: forall (a::k). () => N~k => TypeRep (a::k) -> TypeRep (a::k) pattern Bloop rep <- (foo (typeRep @N) -> Just (HRefl, rep :: TypeRep (a::N))) where Bloop rep = rep }}} Note that I have annotated `rep :: TypeRep (a::N)` in the view pattern, which is the first argument to `Bloop`. Let's reflect that in the type {{{#!hs -- error: -- • Expected kind ‘N’, but ‘a’ has kind ‘k’ -- • In the first argument of ‘TypeRep’, namely ‘(a :: N)’ -- In the type ‘TypeRep (a :: N) -> TypeRep (a :: k)’ -- | -- 15 | pattern Bloop :: forall (a::k). () => N ~ k => TypeRep (a::N) -> TypeRep (a::k) -- | ^ pattern Bloop :: forall (a::k). () => N~k => TypeRep (a::N) -> TypeRep (a::k) pattern Bloop rep <- (foo (typeRep @N) -> Just (rep, HRefl)) where Bloop rep = rep }}} Oh no, GHC complains that `a::k` (not `a::N`) but we have local knowledge that `N ~ k`. I know the rules for kinds are weird so I don't know if this is intended. A way around this is quantifying over an existential variable that is heterogeneously equal to `a`: {{{#!hs pattern Bloop :: forall (a::k). () => forall (n::N). a~~n => TypeRep (n::N) -> TypeRep (a::k) }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14499 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
#14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N) -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: closed Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: duplicate | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #12677 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * status: new => closed * resolution: => duplicate * related: => #12677 Comment: Yes indeed. Here is a simpler version of the issue you've encountered: {{{#!hs {-# LANGUAGE DataKinds, GADTs, PolyKinds, ScopedTypeVariables #-} import Data.Proxy data N = O | S N data Foo (a :: k) where MkFoo :: forall (a :: k). N ~ k => Proxy (a :: N) -> Foo a }}} Here, GHC complains: {{{ GHCi, version 8.2.1: http://www.haskell.org/ghc/ :? for help Loaded GHCi configuration from /home/rgscott/.ghci [1 of 1] Compiling Main ( Bug.hs, interpreted ) Bug.hs:8:45: error: • Expected kind ‘N’, but ‘a1’ has kind ‘k1’ • In the first argument of ‘Proxy’, namely ‘(a :: N)’ In the type ‘Proxy (a :: N)’ In the definition of data constructor ‘MkFoo’ | 8 | MkFoo :: forall (a :: k). N ~ k => Proxy (a :: N) -> Foo a | ^ }}} Despite the fact that GHC is supposed to know that `N ~ k`. Alas, this is due to an unfortunate limitation in how GHC's type system works. I'll quote Richard's comment [https://ghc.haskell.org/trac/ghc/ticket/12677#comment:2 here]:
This is a hard one to fix, surprisingly. The problem is that you've declared `a` to have type `k` and then used `a` as an argument to `->`. Of course, `->` expects a `Type`. So GHC should insert add a cast, forming `a |> η`, for the argument to `->`. The problem is that this would require using the equality proof for `Type ~ k` as the body of `η`, and the current type system simply does not allow this. [https://ghc.haskell.org/trac/ghc/wiki/DependentHaskell/Internal#Liftedvs.Unl... Here] are some notes on the matter, though they were not written to be digested by anyone but me.
I don't expect this will be fixed until we have `-XDependentTypes`.
**tl;dr** GHC's type system probably won't be smart enough to figure this out until dependent types are added. See #12677 for details. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14499#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler
participants (1)
-
GHC