[GHC] #13197: Perplexing levity polymorphism issue

[GHC]

#13197: Perplexing levity polymorphism issue
-------------------------------------+-------------------------------------
           Reporter:  bgamari        |             Owner:
               Type:  bug            |            Status:  new
           Priority:  highest        |         Milestone:  8.2.1
          Component:  Compiler       |           Version:  8.1
  (Type checker)                     |
           Keywords:  typeable       |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  GHC rejects
  Unknown/Multiple                   |  valid program
          Test Case:                 |        Blocked By:
           Blocking:                 |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 I would have expected this to compile since the levity polymorphism patch
 was merged, but sadly it seems the typechecker isn't quite clever enough
 yet (or perhaps I'm the not clever one),
 {{{#!hs
 {-# LANGUAGE GADTs, PolyKinds, PatternSynonyms, RankNTypes,
              TypeOperators, ViewPatterns #-}
 {-# LANGUAGE TypeInType #-}

 module Test where

 import Data.Kind
 import GHC.Exts

 data TypeRep (a :: k) where
   TypeCon :: String -> TypeRep a
   TypeApp :: forall k1 k2 (f :: k1 -> k2) (x :: k1). TypeRep f -> TypeRep
 x -> TypeRep (f x)
   TypeFun :: forall r1 r2 (a :: TYPE r1) (b :: TYPE r2). TypeRep a ->
 TypeRep b -> TypeRep (a -> b)

 data SomeTypeRep where
   SomeTypeRep :: forall k (a :: k). TypeRep a -> SomeTypeRep

 data (a :: k1) :~~: (b :: k2) where
    HRefl :: a :~~: a

 eqTypeRep :: TypeRep (a :: k1) -> TypeRep (b :: k2) -> Maybe (a :~~: b)
 eqTypeRep = undefined

 typeRepKind :: forall (k :: *). forall (a :: k). TypeRep a -> TypeRep k
 typeRepKind = undefined

 toApp :: SomeTypeRep -> SomeTypeRep -> Maybe SomeTypeRep
 toApp (SomeTypeRep f) (SomeTypeRep a)
   | TypeFun arg res <- typeRepKind f
   , Just HRefl <- arg `eqTypeRep` typeRepKind a
   = Just $ SomeTypeRep (TypeApp f a)
 toApp _ _ = Nothing
 }}}

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