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

@@ -2,2 +2,2 @@
- was merged, but sadly it seems the typechecker isn't quite clever enough
- yet (or perhaps I'm the not clever one),
+ (along with Phab:D2038) was merged, but sadly it seems the typechecker
+ isn't quite clever enough yet (or perhaps I'm the not clever one),

New description:

 I would have expected this to compile since the levity polymorphism patch
 (along with Phab:D2038) 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#comment:1>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler