Opened 4 years ago

Closed 4 years ago

#11405 closed bug (fixed)

Incorrect failure of type-level skolem escape check

Reported by: goldfire Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler Version: 8.0.1-rc1
Keywords: TypeInType Cc:
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:

Description (last modified by bgamari)

From Phab:D1739.

When you say

undefined :: forall (v :: Levity). forall (a :: TYPE v). (?callStack :: CallStack) => a

you get a skolem escape failure because GHC things that the kind of (?callStack :: CallStack) => a is TYPE v. It should be *.

I will fix.

Change History (12)

comment:1 Changed 4 years ago by bgamari

Milestone: 8.0.1

I believe this affects the current 8.0 branch as well.

comment:2 Changed 4 years ago by gridaphobe

Priority: normalhighest

Yes, this is a transitive blocker (via #11331) for the 8.0 release.

Last edited 4 years ago by gridaphobe (previous) (diff)

comment:3 Changed 4 years ago by goldfire

I've fixed this (rather simple) problem locally, but it uncovered a deeper one. Consider

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

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?

comment:4 Changed 4 years ago by goldfire

Posted my fix to wip/rae branch.

comment:5 Changed 4 years ago 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.)

comment:6 Changed 4 years ago by goldfire

I agree that we can fix this one problem, but I doubt that it would generalize. I'd like to understand better what's going on here before going down that route.

See NoSubKinds (Issues from Dimitrios) for more information about levity-polymorphic binders. The short answer is that we need to know the runtime size of binders, and we don't know this for levity-polymorphic ones.

comment:7 Changed 4 years ago 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.

comment:8 Changed 4 years ago by simonpj

Richard and I talked about this yesterday. Our provisional solution is to make tcPolyCheck produce a new, simpler form of AbsBinds whose desugaring too can be simpler.


comment:9 Changed 4 years ago by Richard Eisenberg <eir@…>

In bafbde7e/ghc:

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.

comment:10 Changed 4 years ago by Richard Eisenberg <eir@…>

In 3c6635ef/ghc:

Fix #11405.

This adds a new variant of AbsBinds that is used solely for bindings
with a type signature. This allows for a simpler desugaring that
does not produce the bogus output that tripped up Core Lint in
ticket #11405. Should make other desugarings simpler, too.

comment:11 Changed 4 years ago by goldfire

Status: newmerge
Test Case: dependent/should_compile/T11405

This one is finally put to rest. Unwiring undefined should now work.

comment:12 Changed 4 years ago by bgamari

Description: modified (diff)
Resolution: fixed
Status: mergeclosed

This has been merged to ghc-8.0 as 018f866.

Note: See TracTickets for help on using tickets.