Re: [GHC] #14507: Core Lint error with Type.Reflection and pattern synonyms

19 Dec 2017

      #14507: Core Lint error with Type.Reflection and pattern synonyms
-------------------------------------+-------------------------------------
        Reporter:  Iceland_jack      |                Owner:  (none)
            Type:  bug               |               Status:  new
        Priority:  highest           |            Milestone:
       Component:  Compiler          |              Version:  8.2.1
      Resolution:                    |             Keywords:
                                     |  PatternSynonyms
Operating System:  Unknown/Multiple  |         Architecture:
                                     |  Unknown/Multiple
 Type of failure:  None/Unknown      |            Test Case:
      Blocked By:                    |             Blocking:
 Related Tickets:                    |  Differential Rev(s):
       Wiki Page:                    |
-------------------------------------+-------------------------------------

Comment (by simonpj):

 Here's a smaller example
 {{{
 module T14507 where

 import Type.Reflection
 import Data.Kind

 foo :: TypeRep a -> (Bool :~~: k, TypeRep a)
 foo rep = error "urk"

 type family SING :: k -> Type where
   -- Core Lint error disappears with this line:
   SING = (TypeRep :: Bool -> Type)

 pattern RepN :: forall (a::kk). () => Bool~kk => SING a -> TypeRep (a::kk)
 pattern RepN tr <- (foo -> ( HRefl :: Bool:~~:kk
                            , tr :: TypeRep (a::Bool)))

 -- error
 pattern SO x <- RepN (id -> x)
 }}}
 The trouble is that the matcher for `SO` has a type like this
 {{{
 $mSO
   :: forall (r :: TYPE rep) kk (a :: kk).
      TypeRep kk a
      -> (((Bool :: *) ~ (kk :: *)) => TypeRep Bool (a |> co_a2sv) -> r)
      -> (Void# -> r)
      -> r
 }}}
 where that unbound `co_a2sv` actually a coercion derived from the match on
 `(Bool ~ kk)`.  If you like, the real second (continuation) argument of
 `$msO` is more like
 {{{
     -> (forall (co::Bool~kk) -> TypeRep Bool (a |> get-superclass co) -> r
 }}}
 This is bogus because

 * We don't have term-level dependency `forall co -> ...`

 * We can't extract a superclass in a type.

 Richard, I need your help again!

-- 
Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14507#comment:3
GHC http://www.haskell.org/ghc/
The Glasgow Haskell Compiler