#11405: Incorrect failure of type-level skolem escape check -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: new Priority: normal | 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: | -------------------------------------+------------------------------------- Changes (by bgamari): * version: 8.1 => 8.0.1-rc1 * milestone: => 8.0.1 Comment: I believe this affects the current 8.0 branch as well. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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

#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 gridaphobe): Is it just a problem because of `x0`, ie would {{{ x = \ @(v :: Levity) @(a :: TYPE v) ($dict :: (?callStack :: CallStack)) -> let $dict' = ... in undefined @v @a $dict' }}} be OK? If so, can we change the desugarer to not generate the intermediate binder when there's only one use and no recursion? I'm not sure that would be a general fix, but it would fix the immediate problem. (Also, why are levity-polymorphic binders not allowed? Is this explained somewhere? Just curious.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:5 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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): Interestingly, this works on a non-`DEBUG` build, probably because we run Core Lint only after doing the quick optimization pass after desugaring. Perhaps that's a clue to how to solve this... only look for levity- polymorphic binders after the quick optimization pass? Seems a bit odd. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#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 Richard Eisenberg ): In [changeset:"bafbde7e239dd7353fb32cb2ff1b1c9139e4f45c/ghc" bafbde7e/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="bafbde7e239dd7353fb32cb2ff1b1c9139e4f45c" Constrained types have kind * in validity check. This addresses #11405, but a deeper problem lurks. Try test dependent/should_compile/T11405 and see comment:3 on the ticket. }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#11405: Incorrect failure of type-level skolem escape check -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: bug | Status: merge 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: | dependent/should_compile/T11405 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * testcase: => dependent/should_compile/T11405 * status: new => merge Comment: This one is finally put to rest. Unwiring `undefined` should now work. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11405#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler