[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:                    |
-------------------------------------+-------------------------------------

Comment (by goldfire):

 This is expected behavior. Well, for me. After I've studied it and revised
 my expectation.

 The problem is that `k2` in the type of `TypeApp` has kind `Type`. But `f
 a`'s kind, `res`, has type `TYPE r2`, which we see looking at the type of
 `TypeFun`. So we get a type error.

 The fix is to convince GHC that `f a`'s type's kind is really `Type`. And
 we can do that with one extra check:

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

 This compiles for me. Note that `arg`'s kind is discovered to be `Type`
 because `arg` equals the result of a `typeRepKind`, which always has kind
 `Type`.

 Fun times!

 GHC should really come little trophies that you can accrue by triggering
 certain bizarre scenarios.

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