Opened 3 years ago

Closed 3 years ago

Last modified 3 years ago

#12549 closed bug (fixed)

Panic on ":t datatypeName"

Reported by: johnleo Owned by: johnleo
Priority: normal Milestone: 8.2.1
Component: Compiler Version: 8.1
Keywords: Cc:
Operating System: MacOS X Architecture: x86_64 (amd64)
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: #11371 #12785 #12931 Differential Rev(s):
Wiki Page:

Description (last modified by johnleo)

Reproduction:

GHCi, version 8.1.20160826: http://www.haskell.org/ghc/  :? for help
Loaded GHCi configuration from /Users/leo/.ghci
Prelude> :m + GHC.Generics
:m + GHC.Generics
Prelude GHC.Generics> :t datatypeName
:t datatypeName
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160826 for x86_64-apple-darwin):
	ASSERT failed!
  CallStack (from HasCallStack):
  assertPprPanic, called at compiler/types/TyCoRep.hs:2094:44 in ghc:TyCoRep
  checkValidSubst, called at compiler/types/TyCoRep.hs:2122:17 in ghc:TyCoRep
  substTy, called at compiler/typecheck/TcMType.hs:793:24 in ghc:TcMType
  in_scope InScope {k1_a1X8}
  tenv [a1X0 :-> k1_a1X8[tau:3]]
  cenv []
  tys [k_a1X4[tau:3] → (k1_a1X0 → *) → k1_a1X0 → ★]
  cos []
  needInScope [a1X4 :-> k_a1X4[tau:3]]

Please report this as a GHC bug:  http://www.haskell.org/ghc/reportabug

Change History (33)

comment:1 Changed 3 years ago by johnleo

My .ghci file, in case it is relevant:

:set -fprint-explicit-foralls
:set -fprint-explicit-kinds
:set -fprint-unicode-syntax
:set -XUnicodeSyntax

Actually I have turned all of this off and the bug still reproduces, so it doesn't seem to have anything to do with unicode.

Last edited 3 years ago by johnleo (previous) (diff)

comment:2 Changed 3 years ago by johnleo

Version: 8.0.18.1

comment:3 Changed 3 years ago by johnleo

Does not reproduce in 8.0.1. Behavior in 8.0.1 is the following:

:t datatypeName
datatypeName
  ∷ ∀ {d} {t ∷ ★ → (* → *) → ★ → ★} {f ∷ * → *} {a}.
    Datatype ★ d ⇒
    t d f a → [Char]

Note the inconsistent * and . I was trying this out in 8.1 since I'd seen this behavior in 8.0.1 and intended to create a bug for it and fix it (see https://ghc.haskell.org/trac/ghc/ticket/12550). I haven't made any changes to the 8.1 code. It looks like someone else had already been playing in this area.

Last edited 3 years ago by johnleo (previous) (diff)

comment:4 Changed 3 years ago by johnleo

Description: modified (diff)

comment:5 Changed 3 years ago by mpickering

It's possible that the panic also happens in 8.0.1 because it is caused by an assertion failure. Assertions are not turned on in the released builds.

comment:6 in reply to:  5 Changed 3 years ago by johnleo

Replying to mpickering:

It's possible that the panic also happens in 8.0.1 because it is caused by an assertion failure. Assertions are not turned on in the released builds.

Thanks, I didn't know that. Here's an example of a function from Generics which also has strange unicode display behavior, but which does not cause a panic in 8.1:

:t (:*:)
(:*:) ∷ ∀ {g ∷ ★ → *} {p} {f ∷ ★ → *}. f p → g p → (:*:) ★ f g p

comment:7 Changed 3 years ago by johnleo

Owner: set to johnleo

comment:8 Changed 3 years ago by johnleo

Info after further investigation. The following both work fine.

> :set -XPolyKinds
> class C a where f :: a b
> :t f
f ∷ ∀ {k} {b ∷ k} {a ∷ k → ★}. C k a ⇒ a b
> class C a where f :: b a
> :t f
f ∷ ∀ {k} {a ∷ k} {b ∷ k → ★}. C k a ⇒ b a

However at 3 variables every combination fails (I've used +v here to prevent deep instantiation, which is where the failure occurs).

> class C a where f :: a b c
> :t +v f
f ∷ ∀ {k1} {k2} (a ∷ k1 → k2 → ★).
    C k1 k2 a ⇒
    ∀ (b ∷ k1) (c ∷ k2). a b c
> class C a where f :: b a c
> :t +v f
f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k → k1 → ★) (c ∷ k1). b a c
> class C a where f :: b c a
> :t +v f
f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k1 → k → ★) (c ∷ k1). b c a

All three of these panic without the +v. Note that with no PolyKinds everything is fine

> class C a where f :: a b c
> :t f
f ∷ ∀ {b} {a ∷ ★ → ★ → ★} {c}. C a ⇒ a b c

The problem seems to be that in the PolyKinds case with 3 variables, the quantification of some variables is moving to the right of the class constraint. Variables are instantiated in independent groups, with separate groups before and after the constraint, and here the types after the constraint are referring to kinds defined before the constraint, causing the panic.

This likely doesn't panic in 8.0.1. The type signature is different (note that +v is not an option in 8.0.1) with all quantifiers before the constraint.

> class C a where f :: b a c
> :t f
f ∷ ∀ {k} {k1} {a ∷ k} {b ∷ k → k1 → ★} {c ∷ k1}. C k a ⇒ b a c

I will investigate further.

Last edited 3 years ago by johnleo (previous) (diff)

comment:9 Changed 3 years ago by goldfire

Looks to me that you're hot on the case. Let me know if I can be of help.

comment:10 in reply to:  9 Changed 3 years ago by johnleo

Replying to goldfire:

Looks to me that you're hot on the case. Let me know if I can be of help.

If you have any insight as to why some of the universally quantified variables are moved past the class constraint in 8.1 that would be very helpful. Was this on purpose to fix some bug (it's not clear to me if the semantics are different or not), or might it just have been an unintended side-effect of some other change?

comment:11 Changed 3 years ago by goldfire

The types you report (with +v) look the way I would expect them to be in GHC 8.0, as well. Suppose we have

class <cls> <vars> where
  <meth> :: <ty>

Then the type of <meth> is forall <vars>. <cls> <vars> => <ty>. Note that if a method type mentions fresh type variables (that is, those not introduced in the class head), then the method type will be quantified over those variables. So

class C a where
  f :: a b c

is equivalent to

class C a where
  f :: forall b c. a b c

There's clearly something wrong with instantiation here, but the types for the class methods should be the same in 8.0 as in 8.1.

comment:12 in reply to:  11 Changed 3 years ago by johnleo

Replying to goldfire:

There's clearly something wrong with instantiation here, but the types for the class methods should be the same in 8.0 as in 8.1.

Actually as noted above they are in fact different. In 8.0.1:

> class C a where f :: b a c
> :t f
f ∷ ∀ {k} {k1} {a ∷ k} {b ∷ k → k1 → ★} {c ∷ k1}. C k a ⇒ b a c

In 8.1:

> class C a where f :: b a c
> :t +v f
f ∷ ∀ {k} (a ∷ k). C k a ⇒ ∀ {k1} (b ∷ k → k1 → ★) (c ∷ k1). b a c

The bug is then that in 8.1 the k referred to by b tries to reference the kind defined before the class constraint, which is not in scope at that point, causing the panic.

comment:13 Changed 3 years ago by goldfire

But you don't have +v in 8.0. The type that you're seeing has been instantiated and then regeneralized, so all the variable ordering has been forgotten. I still claim that the internal types assigned to f are the same. You just can't ask GHCi for this type in 8.0. You could, though do a pprTrace or traceTc from TcExpr.tcInferId which can print out the uninstantiated type.

In your last sentence: that k really ought to be in scope throughout the type. If it's not, there's your bug!

comment:14 in reply to:  13 Changed 3 years ago by johnleo

Replying to goldfire:

But you don't have +v in 8.0. The type that you're seeing has been instantiated and then regeneralized, so all the variable ordering has been forgotten. I still claim that the internal types assigned to f are the same. You just can't ask GHCi for this type in 8.0. You could, though do a pprTrace or traceTc from TcExpr.tcInferId which can print out the uninstantiated type.

In your last sentence: that k really ought to be in scope throughout the type. If it's not, there's your bug!

OK, I understand. Perhaps it is a bug in 8.0 as well then. The code seems to be instantiating variables in independent groups, in this case the group before the class constraint and then separately the group after the class constraint. If you know a reason for this let me know. Options for fixing it would include doing all the variables together whether they are before or after the constraint, or saving variables from early groups to be in scope for later groups (perhaps the two are essentially equivalent). I'll explore further.

comment:15 Changed 3 years ago by goldfire

Instantiating variables in groups should be OK... but you should also keep track properly of what's in scope and what should be substituted during the instantiation. In other words, once the k has been instantiated, then you should apply the instantiating substitution to the entire body of k, including in the kinds of other bound variables.

comment:16 Changed 3 years ago by johnleo

Note that this bug was "fixed" in https://git.haskell.org/ghc.git/commitdiff/f4a14d6c535bdf52b19f441fe185ea13d62fdc24 (see https://ghc.haskell.org/trac/ghc/ticket/12785) by replacing substTy with substTyUnchecked in new_meta_tv_x (TcMType.hs). See below.

Here is my understanding of the problem. The panic happens for example for this call:

:set -XPolyKinds
class C a where f :: a b c
:type f

Unique names have been simplified for readability.

The original type (all skolem variables) is the following:

∀ {kf} {kh} (a9 ∷ kf → kh → ★).
  C kf kh a9 ⇒
  ∀ (ba ∷ kf) (cb ∷ kh). a9 ba cb

The outer call to deeply instantiate substitutes kf -> kj, kh -> kk, a9 -> al where the new variables are all tau. Theta becomes C kj kk al and we call deeplyinstantiate now on

∀ (ba ∷ kj) (cb ∷ kk). al ba cb

where it attempts to substitute ba -> bp, cb -> cq

Substitutions are created by newMetaTyVars which is defined as follows.

newMetaTyVars = mapAccumLM newMetaTyVarX emptyTCvSubst
    -- emptyTCvSubst has an empty in-scope set, but that's fine here
    -- Since the tyvars are freshly made, they cannot possibly be
    -- captured by any existing for-alls.

Note the comment: kj and kk are free variables in the range of the upcoming substitutions but are not part of the in-scope set. They were however "freshly made" in the outer call.

Now newMetaTyVarX calls new_meta_tv_x which includes this line (before SPJ's change):

kind   = substTy subst (tyVarKind tv)

Note that subst at this point contains the substitutions made prior to the current one, and so is originally empty. So substTy succeeds on ba -> bp (with kind kj), and bp and kj are added to the in-scope set. However on the second attempt cb -> cq (with kind kk), since subst is now non-empty, substTy calls checkValidSubst with arguments subst and [kk]. checkValidSubst does two checks, the second of which (tysColsFVsInScope) fails. This checks that kk is in the in-scope set which consists of {kj, bp}, and thus the panic.

Although I understand the problem, I don't know the best way to fix it. Certainly retaining kk and the others in the in-scope set for the recursive call to deeplyInstantiate would be sufficient, but I'm not sure why it's necessary. No real substitution is being done for kk at this point, so it is not clear why we need to check the substitution invariant. And even if there was a substitution since the variables are fresh there should no risk of capture during alpha-renaming.

While I was investigating this, SPJ made the change mentioned at the top of this note, which is:

kind   = substTyUnchecked subst (tyVarKind tv)
         -- Unchecked because we call newMetaTyVarX from
         -- tcInstBinderX, which is called from tc_infer_args
         -- which does not yet take enough trouble to ensure
         -- the in-scope set is right; e.g. Trac #12785 trips
         -- if we use substTy here

This indicates that there is a more wide-spread problem, so I don't want to make any changes that would break something else. I'm happy to investigate fixing the larger problem, however. In any case I'd appreciate some guidance at this point.

comment:17 Changed 3 years ago by goldfire

Your analysis is spot on. Thank you!

The problem is (as you may have suspected) that comment on newMetaTyVars. It's just plain wrong.

The problem is that we must always obey The substitution invariant from the eponymous Note in TyCoRep:

When calling (substTy subst ty) it should be the case that
the in-scope set in the substitution is a superset of both:

  * The free vars of the range of the substitution
  * The free vars of ty minus the domain of the substitution

new_meta_tv_x takes care to make sure, as it's building the substitution, that the first point is obeyed. But no one is handling the second point!j

Perhaps it was envisioned that nwMetaTyVars would be called only on a closed sequence of tyvars. But the function doesn't say that, and evidently it's not true. (I doubt it ever was!) So it seems the answer is to add an InScopeSet parameter to newMetaTyVars that should contain the free variables of the type being instantiated.

Does that help?

comment:18 Changed 3 years ago by johnleo

Thank you, that is indeed very helpful. I realized when writing my previous two versions of this comment (please ignore them) that I was thinking about substitutions backwards. It does seem the problem and solution are quite straightforward as you say. I will try implementing it.

Last edited 3 years ago by johnleo (previous) (diff)

comment:19 Changed 3 years ago by simonpj

Yes, all the calls to substTyUnchecked indicate places where the in-scope set is not properly maintained. I think most, but not all, of the calls to newMetaTyVarX do have a correct in-scope set. As my comment says, the one that doesn't is the call from tc_infer_args, which is a bit of code that (as Richard knows) I do not fully understand.

Richard: we may need your help to get the in-scope set right here.

John: which call to newMetaTyVars do you think is at fault? They all look ok to me.

Simon

comment:20 Changed 3 years ago by johnleo

It's buried a bit in all the text I wrote above (written when I was still trying to understand the code), but it's the line

  = do { (subst, tvs') <- newMetaTyVars tvs

of deeplyInstantiate, particularly inside the recursive call that happens a few lines down.

       ; (wrap2, rho2) <- deeplyInstantiate orig (substTyUnchecked subst rho)

In the example I give above there are two forall groups. The first works fine and substitutions are made into the second via the substTyUnchecked, in particular into the kind variables of the second group. However these kind variables are not part of the the in-scope set when

              kind   = substTyUnchecked subst (tyVarKind tv)

is called in new_meta_tv_x of the second, recursive, call of deeplyInstantiate, since newMetaTyVars starts with a fresh empty in-scope set, thus the panic I was looking at. As I noted above, the kind variables being substituted into are "fresh" from the outer call and thus there will be no real problem, but it's probably better to pass them in to newMetaTyVars as Richard suggests rather than trying to special-case the checking logic, and there may well still be places where not passing in a pre-existing in-scope set does cause a real problem.

comment:21 Changed 3 years ago by simonpj

Right you are. Here's what to do:

  • Make deeply_instantiate take a substitution that it extends:
    deeply_instantiate :: CtOrigin 
                       -> TCvSubst   -- new!
                       -> TcSigmaType -> TcM (HsWrapper, TcRhoType)
    
    Its semantics are:
    deeply_instantiate subst ty = deeplyInstantiate (substTy subst ty)
    
  • Define deeplyInstantiate (externally called) initialise the substitution with a suitable in-scope set, like this:
    deeplyInstantiate ty = deeply_instantiate (mkEmptyTcSubst (tyCoVarsOfType ty)) ty
    
  • The impl of deeply_instantiate is just as deeplyInstantiate today, except:
    • Use newMetaTyVarsX to extend the substitution
    • The unchecked-ness can go away
    • The recursive call is to deeply_instantiate, and does not substitute in rho.

Make sense?

comment:22 Changed 3 years ago by johnleo

Thank you, everything makes sense except "does not substitute in rho". Perhaps I misunderstood something, but it seems it is essential to substitute into rho at some point and nowhere else is it done, so if I leave that out the original skolem variables are never replaced with taus and unification fails later on. Indeed I tried this out and it failed: I get the error No instance for (C k0 k1 a0) arising from a use of ‘f’ when I try to do :t f for class C a where f :: a b c. If I leave in the substitution for rho everything seems to work fine. Note that I keep the unchecked substitutions in deeply_instantiate and only revert the one in new_meta_tv_x (which was the one causing the bug in the first place), since I'm worried making the other ones checked will cause other problems.

comment:23 Changed 3 years ago by simonpj

everything makes sense except "does not substitute in rho".

Remember:

deeply_instantiate subst ty = deeplyInstantiate (substTy subst ty)

So deeply_instantiate itself is responsible for applying subst to ty, not the caller of deeply_instantiate.

So I did miss something: in the otherwise case, which currently looks like

  | otherwise = return (idHsWrapper, ty)

you'll need to use substTy subst ty.

Also make sure you use newMetaTyVarsX so that you pass in the current substitution and get an extended substitution.

comment:24 Changed 3 years ago by johnleo

Thanks, that also works, and as you say is semantically cleaner. I did in fact use newMetaTyVarsX; in fact I had to write it since it didn't exist, but it is straightforward.

newMetaTyVarsX :: TCvSubst -> [TyVar] -> TcM (TCvSubst, [TcTyVar])
-- Just like newMetaTyVars, but start with an existing substitution.
newMetaTyVarsX subst = mapAccumLM newMetaTyVarX subst

I'll post the code for review in the near future. Note that I haven't handled tc_infer_args.

comment:25 Changed 3 years ago by johnleo

I've posted my change for review: https://phabricator.haskell.org/D2757

As noted there, this does not fix the tc_infer_args problem so we'll either have to defer this checkin until that's fixed or change the substTy in new_meta_tv_x back to substTyUnchecked and file a new bug for tc_infer_args. I wanted to make sure my other changes were okay, however.

comment:26 Changed 3 years ago by goldfire

Regardless of anything else: do please file a bug about the tc_infer_args problem, so that I have something to put in my queue. Otherwise, this seems to be humming nicely to a conclusion.

comment:27 Changed 3 years ago by Ben Gamari <ben@…>

In 2350906/ghc:

Maintain in-scope set in deeply_instantiate (fixes #12549).

Maintain in-scope set in deeply_instantiate (Fixes T12549).

lint fixes

Test Plan: validate

Reviewers: simonpj, austin, goldfire, bgamari

Reviewed By: simonpj, bgamari

Subscribers: thomie

Differential Revision: https://phabricator.haskell.org/D2757

GHC Trac Issues: #12549

comment:28 Changed 3 years ago by bgamari

Milestone: 8.2.1

Thanks John!

Is there a bug describing the tc_infer_args issue mentioned in comment:26? I'll keep this ticket open until one is opened so we don't lose track of this.

comment:29 Changed 3 years ago by johnleo

Thanks for merging! There is a bug #12785 in which Simon changed a substTy to substTyUnchecked and mentions it is due to tc_infer_args not setting up the in-scope set correctly. However I'm not sure if fixing the tc_infer_args problem fixes that bug or if this is a separate issue. Richard and Simon, is it enough to track the tc_infer_args problem in #12785? If not I can create a new bug for it.

comment:30 Changed 3 years ago by simonpj

I'm not certain, but I thought that tc_infer_args was the only caller of new_meta_tv_x which didn't establish the in-scope set.

There are lots of substTyUnchecked which each need individual attention. I suppose a new ticket that enumerated them would be a good thing.

comment:31 Changed 3 years ago by johnleo

comment:32 Changed 3 years ago by johnleo

Resolution: fixed
Status: newclosed

comment:33 Changed 3 years ago by johnleo

I created a new bug for tc_infer_args (#12931) and set the owner to Richard. Regarding other uses of substTyUnchecked, there is already the existing bug #11371, which was left open to address them (see https://ghc.haskell.org/trac/ghc/ticket/11371#comment:51). I count at least 35 calls to substTyUnchecked (run grep substTyUnchecked */*.hs in the compiler directory); I'm not sure if it's worth listing them all in the bug. I'm closing this bug as fixed.

Note: See TracTickets for help on using tickets.