[GHC] #14499: Pattern synonym, (a::k) cannot be written (a::N) given (k ~ N)

[GHC]

#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