#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