#11648 closed bug (fixed)

assertPprPanic, called at compiler/types/TyCoRep.hs:1932

Reported by: thomie Owned by: goldfire
Priority: highest Milestone: 8.0.1
Component: Compiler Version: 8.1
Keywords: TypeInType Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case: polykinds/T11648{,b}
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

As mentioned in https://mail.haskell.org/pipermail/ghc-devs/2016-February/011455.html, the following tests currently hit an assert when the compiler is built with -DDEBUG:

   patsyn/should_compile  MoreEx [exit code non-0] (normal)
   patsyn/should_compile  T11224b [exit code non-0] (normal)
   polykinds              MonoidsTF [exit code non-0] (normal)
   polykinds              T11480b [exit code non-0] (normal)
   polykinds              T11523 [exit code non-0] (normal)
Compile failed (status 256) errors were:
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.1.20160218 for x86_64-unknown-linux):
ASSERT failed!
  CallStack (from HasCallStack):
  assertPprPanic, called at compiler/types/TyCoRep.hs:1932:56 in ghc:TyCoRep
  checkValidSubst, called at compiler/types/TyCoRep.hs:1991:17 in
ghc:TyCoRep
  substTys, called at compiler/types/TyCoRep.hs:2012:14 in ghc:TyCoRep
  substTheta, called at compiler/typecheck/TcPatSyn.hs:255:20 in
ghc:TcPatSyn
  in_scope InScope {d_ap0 c_apv}
  tenv [ap1 :-> c_apv[tau:5]]
  tenvFVs [aps :-> t_aps[tau:1], apv :-> c_apv[tau:5]]
  cenv []
  cenvFVs []
  tys []
  cos []

Phab:D1951 contained a stopgap patch, but since it wasn't accepted, I'll just mark the tests as expect_broken for this ticket, so that other developers aren't bothered by this issue.

The offending commit is b5292557dcf2e3844b4837172230575d40a8917e.

Change History (25)

comment:1 Changed 19 months ago by simonpj

Happily I'm about to commit a proper fix for this. (I think.)

comment:2 Changed 19 months ago by Simon Peyton Jones <simonpj@…>

In b4dfe04/ghc:

Fix kind generalisation for pattern synonyms

We were failing to zonk, after quantifyTyVars, and that left
un-zonked type variables in the final PatSyn.

This fixes the patsyn/ problems in Trac #11648, but not
the polykinds/ ones.

comment:3 Changed 19 months ago by simonpj

Still open: the polykinds/ tests. So leave the ticket open.

But pls merge the above patch to 8.0.

comment:4 Changed 19 months ago by bgamari

Milestone: 8.0.1
Status: newmerge

comment:6 Changed 19 months ago by bgamari

Resolution: fixed
Status: mergeclosed

comment:7 Changed 19 months ago by simonpj

Resolution: fixed
Status: closednew

The polykinds ASSERT errors are not yet fixed.

comment:8 Changed 19 months ago by simonpj

Here's a smaller test case for the polykinds error

class Monoidy (to :: k0 -> k1 -> *) (m :: k1)  where
  type MComp to m :: k1 -> k1 -> k0
  mjoin :: MComp to m m m `to` m

The problem is this:

  • TcTyClsDecls.getFamDeclInitialKind thinks that MComp has a CUSK.
  • When it quantifies over it, it gives it the kind:
      MComp :: forall k1_aLj[sk] (k0_aLi[sk] :: TYPE t_aSB[tau:1]).
               (k0_aLi[sk] -> k1_aLj[sk] -> *)
               -> k1_aLj[sk] -> k1_aLj[sk] -> k1_aLj[sk] -> k0_aLi[sk]
    
    This is wrong: the t_aSB should be instantiated to Lifted. It's terrible for a meta-tyvar to end up in the kind of a TyCon.
  • So I'm worried about where this defaulting happens in TcHsType.kcHsTyVarBndrs with cusk = True. Indeed, by adding tracing to this program I've confirmed that Monoidy also gets a kind (at least during kind-checking) looking like
    forall (k1{tv aLi} [sk] :: *)
           ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q}
                                    (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334}))
            :: TYPE{(w) tc 32Q} (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334})).
           ((k0{tv aLh} [sk] :: TYPE{(w) tc 32Q}
                                   (t_aSs{tv} [tau:1] :: RuntimeRep{(w) tc 334}))
               -> (k1{tv aLi} [sk] :: *) -> *{(w) tc 330})
           -> (k1{tv aLi} [sk] :: *)
           -> Constraint{(w) tc 32Y}
    
    
    Notice that t_aSB.

But even if we fix that I'm worried about doing this CUSK stuff for associated types. I think it's probably wrong. We are crawling over the class decl to find constraints on the kind variables so we can infer the class decl's kind. We start that process with getInitialKinds; and we can't at that moment quantify over the kind variables we are about to gather constraints for!

At very least we must elaborate Note [Complete user-supplied kind signatures] to cover associated types. An associate type should have a CUSK iff (a) its parent class does, and (b) any private tyvars have kind sigs.

I'm a bit puzzled about why we call kcTyClDecl and generaliseTCD at all for decls with a CUSK.

comment:9 Changed 19 months ago by simonpj

Keywords: TypeInType added
Owner: set to goldfire
Priority: normalhighest

Richard, I'm making this 'highest' because it's not just to do with substitutions; there seems to be a clear violation of the invariants about meta-tyvars.

comment:10 Changed 19 months ago by goldfire

I've been wondering if this dragon would bite. And now it has.

Consider

data T (a :: Proxy k)

Does that have a CUSK? According to the CUSK rules for datatypes, it does indeed: all of the type variables have a kind signature. But there's a problem in that we don't know k's type! So this kind signature isn't complete. Instead, we should need to say, e.g.,

data T :: forall (k :: *). Proxy k -> *

Note the explicit :: * on k's binder, which is necessary for us to have completely specify the kind.

However, in looking more closely at this case, I don't actually think this is the problem. A mistake in detecting CUSKness should affect type inference and whether or not we have principal kinds, etc., but it shouldn't produce the drastic failure that we're seeing above. Somehow, it seems that quantifyTyVars is making a mistake. I don't have the ability to test this at the moment (I'm in an intermediate state) but should get to this later this week. I propose to fix the immediate problem (which should be straightforward) and then to delay the debate about CUSKs for another time.

comment:11 Changed 19 months ago by simonpj

I don't think it's anything to do with quantifyTyVars. Under CUSK conditions we don't call quantifyTyVars; instead kcHsTyVarBndrs does something inscrutable to generate the offending kind.

comment:12 Changed 19 months ago by goldfire

But quantifyTyVars is called from kindGeneralize within kcTyClGroup.generalise, no? I agree that, if our CUSK check were totally accurate, we should skip kcTyClDecl and generaliseTCD, but we currently don't. So quantifyTyVars should get called.

Or am I horribly confused?

comment:13 Changed 19 months ago by simonpj

Well maybe it does, but the ASSERT fails because in getInitialKinds because there is a CUSK we compute an initial kind for MComp that contains a unification variable.

Now, if the ASSERT isn't there nothing actually breaks. But it's plainly wrong for MComp to have a kind (even temporarily) that has a free levity variable.

I don't want to fix this by adding this bogus unification variable to the in-scope set; nor by disabling the ASSERT.

But you could argue that since nothing is actually broken this doesn't matter, and the dragon is sleeping.

comment:14 Changed 19 months ago by goldfire

Ah -- so the meta-tyvars aren't making it to the real TyCon, only the TcTyCon? It's quite normal for TcTyCons to have meta-tyvars. (Indeed, that's what they're for.)

But I'm missing some context. The ASSERT that's breaking is the check during substitutions. But which substitution? I don't see an obvious substitution in getFamDeclInitialKind.

To be clear, I think there are two related problems going on:

  1. The CUSK check is inaccurate in the presence of TypeInType, because implicitly-bound kind variables (like k in data Proxy (a :: k)) can have non-trivial types.
  2. The code in TcTyClsDecls is tripping over CUSK types that aren't actually CUSKs.

I propose to fully defer (1). It can be triggered only with TypeInType enabled and has some thorny design issues. And when it goes wrong, it won't be catastrophic (i.e., no panicking, segfaulting, or launching rockets, just an unexpected -- but still sound -- result of type inference).

(2) is the real issue at hand. And, currently without the ability to test, I don't fully understand what's going wrong. I hope to be out of my intermediate state today or tomorrow.

comment:15 in reply to:  14 Changed 19 months ago by simonpj

Ah -- so the meta-tyvars aren't making it to the real TyCon, only the TcTyCon? It's quite normal for TcTyCons to have meta-tyvars. (Indeed, that's what they're for.)

Yes if they are a bare meta-tyvar, but not if they are full polymorphic kind gotten from a CUSK. The whole point about being "complete" is that the signature is fully defined. We experimented with partially-defined signatures and backed off. Complete means complete, and that means no lurking unification variables.

But I'm missing some context. The ASSERT that's breaking is the check during substitutions. But which substitution? I don't see an obvious substitution in getFamDeclInitialKind.

It happens during the immediately following tc_lhs_type; at an occurrence of MComp we find that it has a polymorphic kind and try to instantiate that kind. The instantiation fails with this error. (But it's just a canary in the mine; the real problem is that unification variable lurking in an allegedly-complete signature.

So yes, (2) is the issue at hand. To go back to your example:

data T (a :: Proxy k)

If we are to treat this as a CUSK (and I think we should) we must fix (at that very moment) the kind of k. Fixing it to * is fine, although its a kind-of-arbitrary choice. But fix it we must. I think the place may be in kcHsTyVarBndrs, which I do not fully understand.

comment:16 Changed 19 months ago by goldfire

This is making yet more sense. And it seems that you are proposing:

  • INVARIANT: The kind of a quantified type variable has no meta-tyvars.

We already had that the quantified type variable itself must not be a meta-tyvar. But this invariant goes one step further, in that the set of variables reachable from a quantified tyvar must be devoid of meta-tyvars. Do you agree with this invariant?

And, as for design, it seems you are proposing (forgetting about associated types for the moment):

  • Keep the syntactic definition of CUSK as it is (Note [Complete user-supplied kind signatures] in HsDecls).
  • When a declaration has a CUSK, default any remaining meta-tyvars after getInitialKind.
  • If a meta-tyvar is not defaultable, the program is erroneous.

I'm quite dubious of this design for several reasons. First, this seems strange to users. For example:

data T1 (a :: Proxy k)
data T2 (a :: Proxy k) b

T1 has a CUSK, according to our definition. Thus its k will be defaulted to kind *. T2, though, does not have a CUSK, and so k is not defaulted and has kind k2.

Second, the design seems hard to implement without annoying users. For example:

data T3 (x :: * -> *)
data T4 (a :: T3 k)

T4 has a CUSK, and k should clearly have kind * -> *. But we can't discover that until kcTyClDecl, which is too late. According to the last bullet above, we'll fail at defaulting T4's k's kind and issue an error, even though it's quite obvious what we should do.

So, I must ask: why is it so necessary to have the INVARIANT at the top? I understand this requires expanding the in-scope set for the substitution at hand, but why is that problematic? I don't see what's so bad about a meta-tyvar in a quantified variable's kind.

comment:17 Changed 19 months ago by simonpj

So, I must ask: why is it so necessary to have the INVARIANT at the top?

What if f :: forall k. forall (a :: kappa). blah, where kappa is a kind meta-var. What if kappa was later instantiated to k? Now the type looks quite different.

Indeed kcHsTyVarBndrs goes to some trouble to avoid this

              -- in the CUSK case, we want to default any un-kinded tyvars
              -- See Note [Complete user-supplied kind signatures] in HsDecls
           ; case hs_tvb of
               UserTyVar {}
                 | cusk
                 , not scoped  -- don't default class tyvars
                 -> discardResult $
                    unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
                                                    (tyVarKind tv)

For your T1/T2 example I'm not too bothered. CUSKs mean that the user has specified the complete kind. If you want k to have some other kind than * you can specify that too (I hope).

For T3/T4, note that kdHsTyVarBndrs calls TcHsTyVarBndr_Scoped which in turn calls unifyKind so I think you'll be fine. (BUt there is clearly a missing solveEqualities here!

comment:18 in reply to:  17 Changed 19 months ago by goldfire

Replying to simonpj:

So, I must ask: why is it so necessary to have the INVARIANT at the top?

What if f :: forall k. forall (a :: kappa). blah, where kappa is a kind meta-var. What if kappa was later instantiated to k? Now the type looks quite different.

I'm not sure what you mean by "quite different". Yes, if we get kappa := k, then the type has more dependency, but what's so bad about that?

Indeed kcHsTyVarBndrs goes to some trouble to avoid this

              -- in the CUSK case, we want to default any un-kinded tyvars
              -- See Note [Complete user-supplied kind signatures] in HsDecls
           ; case hs_tvb of
               UserTyVar {}
                 | cusk
                 , not scoped  -- don't default class tyvars
                 -> discardResult $
                    unifyKind (Just (mkTyVarTy tv)) liftedTypeKind
                                                    (tyVarKind tv)

This code is intended to deal with open data/type family declarations, which always have a CUSK, by fiat. It shouldn't trigger in any other case, because all other declaration forms require KindedTyVars to make a CUSK.

For your T1/T2 example I'm not too bothered. CUSKs mean that the user has specified the complete kind. If you want k to have some other kind than * you can specify that too (I hope).

OK.

For T3/T4, note that kdHsTyVarBndrs calls TcHsTyVarBndr_Scoped which in turn calls unifyKind so I think you'll be fine. (BUt there is clearly a missing solveEqualities here!

Yes, I suppose that's true.

But I don't spot a missing solveEqualities anywhere. Did you miss the call toward the top of kcTyClGroup?

Bottom line here: I'm unconvinced about INVARIANT. But it does seem easy enough to implement "all declarations with CUSKs default all meta-tyvars", which solves the main problem here. And then we just punt on INVARIANT. In other words, I wish to address (1) from comment:14, which will then solve (2) on the way.

comment:19 Changed 19 months ago by simonpj

I'm not sure what you mean by "quite different"

Suppose you instantiate f :: forall k. forall (a :: kappa). blah at some call site. Make up a fresh meta-var for k and substitute. We won't substitute for kappa because it isn't k.

Later we unify kappa := k. And now our earlier instantiation of f's type is utterly wrong.

Actually the real INVARIANT is probably this:

  • In any quantified type forall a. blah, all occurrences of a in blah must be manifest: not hidden inside meta-tyvars, especially if they have not been instantiated.

There could in principle be some free meta-tyvars that we somehow know can never be filled in with the quantified type variable. But for top-level types or kinds this is never necessary.

Anyway I agree with your plan. But

But I don't spot a missing solveEqualities anywhere. Did you miss the call toward the top of kcTyClGroup?

I'm still looking at kcHsTyVarBndrs. It builds a polytype with mkSpecForAllTys. It does unification (inside the call to tcHsTyVarBndr_Scoped). I think we need to solve the equalities before we bind the type variables that are mentioned, don't we? Ugh -- that kcHsTyVarBndrs is horribly complicated.

We should probably Skype but I'm out all Thurs.

comment:20 Changed 19 months ago by Richard Eisenberg <eir@…>

In 55577a9/ghc:

Fix #11648.

We now check that a CUSK is really a CUSK and issue an error if
it isn't. This also involves more solving and zonking in
kcHsTyVarBndrs, which was the outright bug reported in #11648.

Test cases: polykinds/T11648{,b}

This updates the haddock submodule.

[skip ci]

comment:21 Changed 19 months ago by goldfire

Status: newmerge
Test Case: polykinds/T11648{,b}

This one was a bit more pervasive than I first thought to solve, but it probably should be merged.

comment:22 Changed 19 months ago by goldfire

A few comments for posterity on the commit above:

A lot of the changes are due to moving decisions out from kcHsTyVarBndrs, and thus the need to store information in the AST:

  • It turned out to be more convenient to decide if a data decl has a CUSK in the renamed than on the fly. (It could be done on the fly, but it would have been a bit hairy and duplicated code in the renamer.) See the new bit in the manual for a description of what's going on here.
  • There also needed to be a decision about whether to use Anon or Named when building the TcTyBinders of a tycon's kind. Previous to this patch, this was done in kcHsTyVarBndrs, but -- as Simon pointed out to me -- this was bogus (it looked at the free variables of a not-yet-solved-or-zonked type). So it's now done via a simple syntactic check in the renamer. But then the result of the check must be put in the AST, causing knock-on changes. See Note [Dependent LHsQTyVars] in TcHsType and also a new bit in the manual.
  • One of this issues brought up in the ticket is the handling of CUSKs for associated type families. An associated type/data family's CUSKness must be inherited from the enclosing class. Previously, all associated families had CUSKs, but this was wrong. So the CUSK check is a bit more intricate to allow for this relationship.
  • Along the way, I made (->), when used in a kind, have type * -> * -> *, instead of being polymorphic in RuntimeReps. We don't have type-level representation polymorphism.
  • Also incidental to this patch, I made kind variables have kind * when -XTypeInType is not in effect. Not doing this earlier was an oversight. The check isn't perfect, as it's sometimes hard to tell what's a kind variable and what isn't; currently, only variables used in kinds in tycon LHsQTyVars are affected, and these are surely kind variables. (This is mk_kv_kinds in kcHsTyVarBndrs.)
  • There is a new function anonymiseTyBinders. This was necessary in an earlier version of this patch but is now redundant (and harmless). I will remove.

comment:23 Changed 19 months ago by Richard Eisenberg <eir@…>

In 19be5385/ghc:

Remove redundant anonymiseTyBinders (#11648)

This was necessary in an earlier version of the patch for #11648,
but not in the final version. I forgot to remove it.

comment:24 Changed 19 months ago by goldfire

Don't forget to merge both 55577a9 (the main patch) and 19be5385. Thanks!

comment:25 Changed 19 months ago by bgamari

Resolution: fixed
Status: mergeclosed
Note: See TracTickets for help on using tickets.