#11405: Incorrect failure of type-level skolem escape check -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 8.0.1-rc1 Resolution: | Keywords: TypeInType 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 goldfire): I've fixed this (rather simple) problem locally, but it uncovered a deeper one. Consider {{{#!hs x :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a x = undefined }}} Looks innocent enough. But disaster ensues with the generated core, which is like this: {{{ x = \ @(v :: Levity) @(a :: TYPE v) ($dict :: (?callStack :: CallStack)) -> let $dict' = ... in letrec x0 :: a x0 = undefined @v @a $dict' in x0 }}} The problem here is that `x0` is an abomination -- a levity-polymorphic binder, which we have decided are not allowed. This one is harmless (I think), but Core Lint doesn't know that. Any good ideas of how to proceed? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler