[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 (Type    |              Version:  8.0.1
  checker)                           |
      Resolution:                    |             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:                    |
-------------------------------------+-------------------------------------
Description changed by bgamari:

@@ -67,3 +67,0 @@
-
- Adding a `FunCo` constructor to `Coercion` would likely be an easy way to
- resolve this.

New description:

 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]`.

--

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