un-wire-in error, undefined, CallStack, and IP
ClosedPublic

Authored by gridaphobe on Jan 5 2016, 4:41 PM.

Details

Summary

I missed a crucial step in the wiring-in process of CallStack in D861, the bit where you actually wire-in the Name... This led to a nasty bug where GHC thought CallStack was not wired-in and tried to fingerprint it, which failed because the defining module was not loaded.

But we don't need CallStack to be wired-in anymore since error and undefined no longer need to be wired-in. So we just remove them all.

Test Plan

./validate and make slowtest TEST=tc198

Diff Detail

Repository
rGHC Glasgow Haskell Compiler
Lint
Automatic diff as part of commit; lint not applicable.
Unit
Automatic diff as part of commit; unit tests not applicable.
gridaphobe updated this revision to Diff 6083.Jan 5 2016, 4:41 PM
gridaphobe retitled this revision from to wire-in CallStack correctly.
gridaphobe updated this object.
gridaphobe edited the test plan for this revision. (Show Details)
gridaphobe set the repository for this revision to rGHC Glasgow Haskell Compiler.
gridaphobe added a project: GHC.
gridaphobe updated the Trac tickets for this revision.
simonpj accepted this revision.Jan 5 2016, 5:50 PM
simonpj added a reviewer: simonpj.
This revision is now accepted and ready to land.Jan 5 2016, 5:50 PM

Hmm, validate is throwing an ugly error:

931 libraries/base/GHC/Stack/Types.hs:106:3: error:
932	    • GHC internal error: ‘EmptyCallStack’ is not in scope during type checking, but it passed the renamer
933	      tcl_env of environment: [08l :-> Identifier[emptyCallStack::CallStack, <TopLevel>],
934	                               08m :-> Identifier[pushCallStack::([Char], SrcLoc)
935	                                                                 -> CallStack
936	                                                                 -> CallStack, <TopLevel>],
937	                               a8c :-> Identifier[stk::CallStack, <NotTopLevel>],
938	                               r89 :-> Identifier[getCallStack::CallStack
939	                                                                -> [([Char], SrcLoc)], <TopLevel>],
940	                               r8a :-> Identifier[freezeCallStack::CallStack
941	                                                                   -> CallStack, <TopLevel>]]
942	    • In the pattern: EmptyCallStack
943	      In a case alternative: EmptyCallStack -> []
944	      In the expression:
945	        case stk of {
946	          EmptyCallStack -> []
947	          PushCallStack cs stk' -> cs : getCallStack stk'
948	          FreezeCallStack stk' -> getCallStack stk' }

I suspect this is due to callStackTyCon not listing its constructors. The reason is that CallStack contains a SrcLoc, but I wanted to avoid wiring-in SrcLoc as it's a large type and there's no reason to do so beyond the reference from CallStack. I think the CallStack datacons really just need a known-key name for SrcLocs tycon, which we already have, but the types don't work out unfortunately.

Is there a clean way to avoid wiring-in SrcLoc here? It's not a big deal to wire it in, but it's a bit anti-modular..

Wiring-in is transitive. As it stands there is no way to have CallStack wired-in without SrcLoc being so too.

Best thing is NOT to wire-in CallStack. Why is it wired in? Only because it's used in the types of eRROR_ID and uNDEFINED_ID. Why are they wired-in? I have no idea.

Let's un-wire-in eRROR_ID, uNDEFINED_ID, and CallStack. See if that works.

Simon

bgamari edited edge metadata.Jan 6 2016, 4:21 AM

@simonpj, don't we need to attach strictness information to eRROR_ID and uNDEFINED_ID (namely to indicate that they are bottoming)?

Bother. eRROR_ID and uNDEFINED_ID are wired in not because of their strictness (which will be inferred) but because they are levity-polymorphic.

But levity polymorphism seems to be lost:

f x = error x

doesn't become levity polymorphic even though error is. We'll have to ask Richard why not.

Bother bother. I don't want to wire in CallStack etc just to get levity polymorphism for error!! That's stupid.

Let's check with Richard first

gridaphobe edited edge metadata.Jan 6 2016, 10:42 AM
gridaphobe added a subscriber: goldfire.

Bother. eRROR_ID and uNDEFINED_ID are wired in not because of their strictness (which will be inferred) but because they are levity-polymorphic.

But levity polymorphism seems to be lost:

f x = error x

doesn't become levity polymorphic even though error is. We'll have to ask Richard why not.

Bother bother. I don't want to wire in CallStack etc just to get levity polymorphism for error!! That's stupid.

Let's check with Richard first

eRROR_ID and uNDEFINED_ID were originally wired-in because they had an OpenKind, which couldn't be specified in source Haskell. Now that we have levity-polymorphism (which IIRC can be specified in source Haskell) we should be able to un-wire them, and by extension un-wire CallStack and IP.

@goldfire, is this correct?

@gridaphobe, I believe so and I gave it a shot in D1743.

@goldfire, I have a couple questions about levity-polymorphism.

I'm trying to un-wire-in error and undefined, which means giving the definitions in GHC.Err the proper levity-polymorphic signatures. I believe those are

error     :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => [Char] -> a
undefined :: forall (v :: Levity) (a :: TYPE v). (?callStack :: CallStack) => a

and the types in MkCore seem to confirm. But I'm running into a few problems..

  1. GHC gives the following warning for error
libraries/base/GHC/Err.hs:43:34: warning:
    Unused quantified type variable ‘(v :: Levity)’
    In the type ‘forall (v :: Levity) (a :: TYPE v). [Char] -> a’

with the above type, but it goes away if I add a second forall, eg

error :: forall (v :: Levity). forall (a :: TYPE v). (?callStack :: CallStack) => [Char] -> a

I find this confusing because I would expect the two to be equivalent.

  1. GHC won't accept undefined at all, giving the following error
libraries/base/GHC/Err.hs:72:14: error:
    • Quantified type's kind mentions quantified type variable
      (skolem escape)
           type: forall (v1 :: Levity) (a1 :: TYPE v1).
                 (?callStack::CallStack) =>
                 a1
        of kind: TYPE v
    • In the type signature:
        undefined :: forall (v :: Levity).
                     forall (a :: TYPE v). (?callStack :: CallStack) => a

Why is this a problem for undefined, but not for error? The only difference is the extra function parameter.

gridaphobe updated this revision to Diff 6108.Jan 7 2016, 11:32 AM
gridaphobe retitled this revision from wire-in CallStack correctly to un-wire-in error, undefined, CallStack, and IP.
gridaphobe updated this object.
gridaphobe edited the test plan for this revision. (Show Details)

un-wire-in error and friends

goldfire edited edge metadata.Jan 11 2016, 6:44 AM

What you're doing is spot on. What GHC is doing in response is bogus.

See new tickets Trac #11404 and Trac #11405.

I'm getting confused here.

Our goal, triggered by Trac #11331, is not to wire-in undefined or error. (Why? Because doing so forces us to wire-in CallStack)

So we want them to have types

error :: forall (a :: TYPE v). ?loc:::CallStack => String -> a
undefined :: forall (a:: Type v). ?loc::CallStack => a

(Notice that these are not the types they have in Haskell 98, but they are the types given in MkCore.)
I think these are both OK because the arrows mean that the kind of the thing inside the forall is of kind *.

But I think Richard is saying that

bad_udefined :: forall (a:TYPE v). a

is not allowed, for good reasons.

Do we need it? Do we want it? If we do need it, do we have to wire it in? And how will it work?

gridaphobe updated this revision to Diff 6149.Jan 11 2016, 12:09 PM
gridaphobe edited edge metadata.

rebase and fix conflict

gridaphobe updated this revision to Diff 6154.Jan 11 2016, 3:54 PM
gridaphobe edited edge metadata.

appease -Werror

But I think Richard is saying that

bad_udefined :: forall (a:TYPE v). a

is not allowed, for good reasons.

Do we need it? Do we want it? If we do need it, do we have to wire it in? And how will it work?

To quote Simon whenever I discuss roles in kinds: "No no no! Nein!"

We simply don't need this type. Perhaps we could come up with some special-case way to get it, but we don't need it. Anyone who writes this type gets a type error.

gridaphobe updated this revision to Diff 6157.Jan 11 2016, 5:37 PM
gridaphobe edited edge metadata.

sigh, fix haddock

bgamari requested changes to this revision.Jan 13 2016, 7:38 AM
bgamari edited edge metadata.

Looks like we still have validation issues.

This revision now requires changes to proceed.Jan 13 2016, 7:38 AM

Yes, they're mostly of the form

+     Cannot instantiate unification variable ‘a0’
+      with a type involving foralls: (forall a1. a1 -> a1) -> a
+        GHC doesn't yet support impredicative polymorphism
+ In the expression: undefined :: (forall a. a -> a) -> a

I suspect these examples used to type check because undefined had an open kind and perhaps ghc ignored the impredicativity there. In the current patch undefined has a lifted kind so ghc complains about the impredicativity.

I wonder what will happen when we give undefined the levity-polymorphic type, will ghc still complain? @goldfire?

There's also this error:

Actual stderr output differs from expected:
--- ./simplCore/should_compile/spec-inline.stderr.normalised	2016-01-12 00:14:48.334940998 +0000
+++ ./simplCore/should_compile/spec-inline.comp.stderr.normalised	2016-01-12 00:14:48.334940998 +0000
@@ -32,7 +32,7 @@
 
 -- RHS size: {terms: 2, types: 2, coercions: 0}
 Roman.foo3 :: Int
-[GblId, Str=DmdType x]
+[GblId, Str=DmdType b]
 Roman.foo3 =
   Control.Exception.Base.patError
     @ 'GHC.Types.Lifted
*** unexpected failure for spec-inline(optasm)

This concerns me because it seems to have something to do with the strictness information, which shouldn't have changed. I don't know what DmdType x vs DmdType b means though.

I suspect these examples used to type check because undefined had an open kind and perhaps ghc ignored the impredicativity there. In the current patch undefined has a lifted kind so ghc complains about the impredicativity.

I wonder what will happen when we give undefined the levity-polymorphic type, will ghc still complain? @goldfire?

I think it will still complain and rightly so. Let's see the examples.

-[GblId, Str=DmdType x]
+[GblId, Str=DmdType b]

I have made a change to the demand analyser, fixing Trac #11222 which introduced the b -> x change. I don't know why that change didn't induce the same diff in the test though.

I wonder what will happen when we give undefined the levity-polymorphic type, will ghc still complain? @goldfire?

I think it will still complain and rightly so. Let's see the examples.

Using error (which is levity-polymorphic in the current patch) as a proxy I get

ghci> :t error
error
  :: forall (v :: GHC.Types.Levity) (a :: TYPE v).
     (?callStack::GHC.Stack.Types.CallStack) =>
     [Char] -> a

ghci> :t error "bad" :: (forall a. a -> a) -> a
error "bad" :: (forall a. a -> a) -> a
  :: (?callStack::GHC.Stack.Types.CallStack) =>
     (forall a1. a1 -> a1) -> a

ghci> :t undefined
undefined :: (?callStack::GHC.Stack.Types.CallStack) => a

ghci> :t undefined :: (forall a. a -> a) -> a

<interactive>:1:1: error:
    • Cannot instantiate unification variable ‘a0’
      with a type involving foralls: (forall a1. a1 -> a1) -> a
        GHC doesn't yet support impredicative polymorphism
    • In the expression: undefined :: (forall a. a -> a) -> a

ghci> :t error "bad" :: (forall a. a -> a) -> a
error "bad" :: (forall a. a -> a) -> a

:: (?callStack::GHC.Stack.Types.CallStack) =>
   (forall a1. a1 -> a1) -> a

That should fail; it requires impredicative polymorphism. Make a ticket!

ghci> :t undefined :: (forall a. a -> a) -> a

That should fail too, for the same reason. And it does.

ghci> :t error "bad" :: (forall a. a -> a) -> a
error "bad" :: (forall a. a -> a) -> a

:: (?callStack::GHC.Stack.Types.CallStack) =>
   (forall a1. a1 -> a1) -> a

That should fail; it requires impredicative polymorphism. Make a ticket!

It was decided some time ago (nothing to do with me!) that this should be accepted. And it should for undefined. And it will for undefined once undefined is levity-polymorphic.

See Note [Levity polymorphic variables accept foralls] in TcMType.

It was decided some time ago (nothing to do with me!) that this should be accepted. And it should for undefined. And it will for undefined once undefined is levity-polymorphic.

See Note [Levity polymorphic variables accept foralls] in TcMType.

Ugh1: this note appears twice in the file, with two slightly different titles. Richard, worth fixing.

Ugh2: the implementation uses ReturnTvs which we are busy getting rid of. And which we do not expect to see nested; but now they are. Sigh.

Ugh3: I bet this is my fault. But the note says "So we also allow such type variables
to be instantiate with foralls. It's a bit of a hack, but seems straightforward." But it's not really straightforward. It's really impredicative polymorphism and that's a swamp. It may be that the incredibly-restricted ways in which we allow levity-polymorphic type to appear are also just enough to make impredicative types ok. But I am far from sure this is the case.

I'm strongly inclined to row back from this and require you to eta-expand in such cases. It's not a great imposition, whereas it is a hack that has entirely unclear consequences.

I've filed Trac #11431 so we have a separate place to discuss whether ghc should instantiate levity-polymorphic type variables with foralls.

gridaphobe updated this revision to Diff 6228.Jan 15 2016, 3:28 PM
gridaphobe edited edge metadata.

giving undefined a levity-polymorphic type works now

@bgamari this patch should be good to merge now.

bgamari accepted this revision.Jan 18 2016, 2:44 AM
bgamari edited edge metadata.

Looks good. It feels good to rip out all of this wiring.

This revision is now accepted and ready to land.Jan 18 2016, 2:44 AM
This revision was automatically updated to reflect the committed changes.