[GHC] #12905: Core lint with pattern synonym

[GHC]

#12905: Core lint with pattern synonym
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  normal         |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.0.1
  (Type checker)                     |
           Keywords:  typeable       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  Compile-time
  Unknown/Multiple                   |  crash or panic
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Yet another program from the type-indexed `Typeable` effort which breaks
 GHC (`master` branch as of 3bd1dd4d75fde3b922d4de08c16f29bdeb8e05d7) with
 a core lint error,

 {{{#!hs
 {-# LANGUAGE GADTs, TypeOperators, PatternSynonyms, TypeInType, PolyKinds,
 RankNTypes #-}
 module T where

 import GHC.Exts
 import Data.Kind
 import Data.Type.Equality

 data TypeRep (a :: k) where
     TrTyCon :: TypeRep (a :: k)
     TrApp   :: forall k1 k2 (a :: k1 -> k2) (b :: k1).
                TypeRep (a :: k1 -> k2)
             -> TypeRep (b :: k1)
             -> TypeRep (a b)
     TrFun   :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (a :: TYPE r1)
 (b :: TYPE r2).
                TypeRep a
             -> TypeRep b
             -> TypeRep (a -> b)

 pattern TRFun :: forall k (fun :: k). ()
               => forall (r1 :: RuntimeRep) (r2 :: RuntimeRep) (arg :: TYPE
 r1) (res :: TYPE r2). (k ~ Type, fun ~~ (arg -> res))
               => TypeRep arg
               -> TypeRep res
               -> TypeRep fun
 pattern TRFun arg res <- TrFun arg res
   where TRFun arg res = TrFun arg res
 }}}

 This program produces many core lint errors, although all of them fall
 into only a few classes. Here's one,
 {{{
 *** Core Lint errors : in result of Desugar (before optimization) ***
 <no location info>: warning:
     In the coercion ‘Sym (Sym cobox_a3fT |> Sym cobox_a3fU)’
     Kind application error in
       type ‘((->) |> <*>_N ->_N <*>_N ->_N Sym cobox) a’
       Function kind = * -> * -> k
       Arg kinds = [(a, TYPE r1)]
 }}}

 {{{
 <no location info>: warning:
     [RHS of $d~~_a3fO :: (fun :: k) ~~ ((a -> b) :: *)]
     Kind application error in
       coercion ‘Sym
                   (Sym
                      (<(->)>_N |> ((<*>_N -> <*>_N -> Sym cobox_a3fU)
                                    ; Sym (<*>_N -> <*>_N -> Sym
 cobox_a3fH))) |> (<*>_N
 -> <*>_N
 -> Sym
 cobox_a3fU)) <a>_N’
       Function kind = * -> * -> *
       Arg kinds = [(a, TYPE r1)]
 }}}

 It appears that this is yet another case of the kind of `(->)` being too
 restrictive (#11714) since `a -> b` appears to be lifted to the coercion
 `TyConAppCo role (->) [a, b]`.

 Adding a `FunCo` constructor to `Coercion` would likely be an easy way to
 resolve this.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/12905>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler