Opened 2 years ago

Last modified 2 years ago

#13959 new bug

substTyVar's definition is highly dubious

Reported by: RyanGlScott Owned by: goldfire
Priority: normal Milestone:
Component: Compiler Version: 8.0.1
Keywords: Cc: goldfire
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: None/Unknown Test Case:
Blocked By: Blocking:
Related Tickets: Differential Rev(s):
Wiki Page:

Description

Currently, we have:

substTyVar :: TCvSubst -> TyVar -> Type
substTyVar (TCvSubst _ tenv _) tv
  = ASSERT( isTyVar tv )
    case lookupVarEnv tenv tv of
      Just ty -> ty
      Nothing -> TyVarTy tv

But as Richard pointed out to me, the Nothing case is flat-out wrong. If tv isn't in the substitution, we need to check if any of the variables in tv's kind are in the substitution, and if so, apply the substitution to them.

Fixing this might seem straightforward enough:

  • compiler/types/TyCoRep.hs

    diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
    index 5ac63e5..4f7d650 100644
    a b subst_ty subst ty 
    21912191    go (CoercionTy co)   = CoercionTy $! (subst_co subst co)
    21922192
    21932193substTyVar :: TCvSubst -> TyVar -> Type
    2194 substTyVar (TCvSubst _ tenv _) tv
     2194substTyVar subst@(TCvSubst _ tenv _) tv
    21952195  = ASSERT( isTyVar tv )
    21962196    case lookupVarEnv tenv tv of
    21972197      Just ty -> ty
    2198       Nothing -> TyVarTy tv
     2198      Nothing -> TyVarTy (updateTyVarKind (substTyUnchecked subst) tv)
    21992199
    22002200substTyVars :: TCvSubst -> [TyVar] -> [Type]
    22012201substTyVars subst = map $ substTyVar subst

But note that I'm using substTyUnchecked, not substTy, since if you try using the latter, GHC will pretty quickly fall over on a ./validate --slow build, as substTy's assertions are violated all over the place.

I'm fairly certain I know why the assertions would be tripping up, however. To build most of the in-scope sets used for substTyVar's substitutions, the mkVarSet :: [Var] -> VarSet function is used. But mkVarSet only grabs the Uniques of the type variables themselves, not the variables in the kind of each type variable. This means the in-scope sets will frequently be too narrow to encompass the kind variables, which absolutely must be in the set if we want to change substTyVar as described above.

I'm not sure what the solution is here. Perhaps we should be using a variant of mkVarSet called mkTyVarSet that grabs the Uniques of the kind variables as well?

Change History (17)

comment:1 Changed 2 years ago by goldfire

Thanks for digging into this further. My question is: where do the arguments to mkVarSet come from? Why don't they already have the kind variables in the lists? (They probably should!) My hunch is that the assertion failures you're seeing are genuine -- that is, they suggest real latent bugs.

So, I propose this solution: keep digging! :)

More concretely, point us to a small sampling (1 might be a suitable small number) of places where this mkVarSet call happens, and see if you can describe the context for where that list of variables comes from.

comment:2 Changed 2 years ago by RyanGlScott

Well looking at the definition of mkVarSet, it's no surprise that things are going awry:

mkVarSet :: [Var] -> VarSet
mkVarSet = mkUniqSet

mkUniqSet :: Uniquable a => [a]  -> UniqSet a
mkUniqSet = foldl' addOneToUniqSet emptyUniqSet

It's just grabbing the Unique of each type variable, and nothing more.

Experimentally, when I tried a debugging build of GHC with the modified version of substTyVar, it fell over trying to compile Data.Type.Equality. I don't have the full assertion failure at the moment, but I recall that there were indeed more tenvFVs than what were contained in the in_scope set.

Here's a sample call to mkVarSet that's propagated through to substTyVars. This is used in the logic for GeneralizedNewtypeDeriving, where we need to take all the type variables mentioned in the instance head in preparation for the substitution that substitutes the class tyvars with the types used when deriving the instance.

...Although now that I think about it, this probably isn't a very good example of the thing we're worried about in this ticket, since that substitution is formed by simply zipping the class tyvars with their instantiated types in the instance, so there's no need to ever substitute in the kind of a tyvar... I think.

comment:3 Changed 2 years ago by RyanGlScott

Here's a much more detailed stack trace when compiling Data.Type.Equality:

$ inplace/bin/ghc-stage2 -fforce-recomp -O2 -DDEBUG -dcore-lint Bug.hs
[1 of 1] Compiling Data.Type.Equality ( Bug.hs, Bug.o )
ghc-stage2: panic! (the 'impossible' happened)
  (GHC version 8.3.20170712 for x86_64-unknown-linux):
	ASSERT failed!
  in_scope InScope {k1_X49O a_X49V b_X49X}
  tenv [X49T :-> k1_X49O, X49V :-> a_X49V, X49X :-> b_X49X]
  tenvFVs [X49M :-> k2_X49M, X49O :-> k1_X49O, X49V :-> a_X49V,
           X49X :-> b_X49X]
  cenv []
  cenvFVs []
  tys [*]
  cos []
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1188:22 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep
        substTy, called at compiler/types/TyCoRep.hs:2198:44 in ghc:TyCoRep
  Call stack:
      CallStack (from HasCallStack):
        prettyCurrentCallStack, called at compiler/utils/Outputable.hs:1133:58 in ghc:Outputable
        callStackDoc, called at compiler/utils/Outputable.hs:1137:37 in ghc:Outputable
        pprPanic, called at compiler/utils/Outputable.hs:1186:5 in ghc:Outputable
        assertPprPanic, called at compiler/types/TyCoRep.hs:2089:56 in ghc:TyCoRep
        checkValidSubst, called at compiler/types/TyCoRep.hs:2122:29 in ghc:TyCoRep
        substTy, called at compiler/types/TyCoRep.hs:2198:44 in ghc:TyCoRep
CallStack (from -prof):
  Panic.panic (compiler/utils/Panic.hs:(182,1)-(186,68))
  Outputable.pprDebugAndThen (compiler/utils/Outputable.hs:(1191,1)-(1194,43))
  ErrUtils.prettyPrintGhcErrors.\ (compiler/main/ErrUtils.hs:(658,23)-(666,44))
  GhcMonad.gcatch.\.\ (compiler/main/GhcMonad.hs:117:46-63)
  Panic.throwGhcException (compiler/utils/Panic.hs:171:1-35)
  Panic.panicDoc (compiler/utils/Panic.hs:192:1-61)
  Outputable.pprPanic (compiler/utils/Outputable.hs:1137:1-49)
  Outputable.assertPprPanic (compiler/utils/Outputable.hs:(1185,1)-(1188,35))
  TyCoRep.checkValidSubst (compiler/types/TyCoRep.hs:(2088,1)-(2113,57))
  TyCoRep.substTy (compiler/types/TyCoRep.hs:(2120,1)-(2123,45))
  Var.updateTyVarKind (compiler/basicTypes/Var.hs:456:1-64)
  TyCoRep.substTyVar (compiler/types/TyCoRep.hs:(2194,1)-(2198,61))
  TyCoRep.subst_ty.go (compiler/types/TyCoRep.hs:(2176,5)-(2191,60))
  TyCoRep.subst_ty (compiler/types/TyCoRep.hs:(2173,1)-(2191,60))
  TyCoRep.subst_co.go_ty (compiler/types/TyCoRep.hs:2240:5-26)
  TyCoRep.subst_co.go (compiler/types/TyCoRep.hs:(2243,5)-(2264,66))
  TyCoRep.subst_co (compiler/types/TyCoRep.hs:(2236,1)-(2270,36))
  TyCoRep.substCoUnchecked (compiler/types/TyCoRep.hs:(2223,1)-(2225,33))
  TyCoRep.substCoWithUnchecked (compiler/types/TyCoRep.hs:(2045,1)-(2047,41))
  Coercion.mkInstCo (compiler/types/Coercion.hs:(950,1)-(952,31))
  CoreOpt.pushCoTyArg.co2 (compiler/coreSyn/CoreOpt.hs:1012:5-62)
  CoreOpt.pushCoTyArg (compiler/coreSyn/CoreOpt.hs:(990,1)-(1012,62))
  Simplify.simplCast.addCoerce (compiler/simplCore/Simplify.hs:(1427,8)-(1461,53))
  Simplify.simplCast (compiler/simplCore/Simplify.hs:(1421,1)-(1461,53))
  Simplify.rebuildCall (compiler/simplCore/Simplify.hs:(1761,1)-(1853,47))
  Simplify.completeCall (compiler/simplCore/Simplify.hs:(1718,1)-(1749,60))
  Simplify.simplIdF (compiler/simplCore/Simplify.hs:(1680,1)-(1712,53))
  Simplify.simplExprC (compiler/simplCore/Simplify.hs:(1035,1)-(1041,42))
  Simplify.simplExpr (compiler/simplCore/Simplify.hs:(1018,1)-(1026,45))
  Simplify.simplLam (compiler/simplCore/Simplify.hs:(1501,1)-(1538,37))
  Simplify.simplExprF1 (compiler/simplCore/Simplify.hs:(1064,1)-(1140,52))
  Simplify.simplExprF (compiler/simplCore/Simplify.hs:(1049,1)-(1059,26))
  Simplify.simplLazyBind (compiler/simplCore/Simplify.hs:(381,1)-(432,68))
  Simplify.simplBind (compiler/simplCore/Simplify.hs:(362,1)-(368,58))
  Simplify.simplRecOrTopPair.trace_bind (compiler/simplCore/Simplify.hs:(330,5)-(334,56))
  Simplify.simplRecOrTopPair (compiler/simplCore/Simplify.hs:(321,1)-(334,56))
  Simplify.simplTopBinds.simpl_bind (compiler/simplCore/Simplify.hs:(268,5)-(272,65))
  Simplify.simplTopBinds.simpl_binds (compiler/simplCore/Simplify.hs:(264,5)-(266,64))
  Simplify.simplTopBinds (compiler/simplCore/Simplify.hs:(248,1)-(272,65))
  SimplCore.SimplTopBinds (compiler/simplCore/SimplCore.hs:758:29-64)
  SimplMonad.initSmpl (compiler/simplCore/SimplMonad.hs:(72,1)-(78,36))
  SimplCore.simplifyPgmIO.do_iteration (compiler/simplCore/SimplCore.hs:(691,5)-(798,48))
  SimplCore.simplifyPgmIO (compiler/simplCore/SimplCore.hs:(658,1)-(800,47))
  IOEnv.liftIO (compiler/utils/IOEnv.hs:188:5-33)
  CoreMonad.liftIO (compiler/simplCore/CoreMonad.hs:615:5-37)
  CoreMonad.liftIOWithCount (compiler/simplCore/CoreMonad.hs:619:1-87)
  SimplCore.simplifyPgm (compiler/simplCore/SimplCore.hs:(644,1)-(649,48))
  SimplCore.Simplify (compiler/simplCore/SimplCore.hs:456:40-55)
  SimplCore.doCorePass (compiler/simplCore/SimplCore.hs:(455,1)-(500,50))
  SimplCore.runCorePasses.do_pass (compiler/simplCore/SimplCore.hs:(442,5)-(450,28))
  SimplCore.runCorePasses (compiler/simplCore/SimplCore.hs:(439,1)-(452,24))
  IOEnv.thenM.\ (compiler/utils/IOEnv.hs:(83,37)-(84,60))
  IOEnv.thenM (compiler/utils/IOEnv.hs:(83,1)-(84,61))
  CoreMonad.>>=.\ (compiler/simplCore/CoreMonad.hs:(524,30)-(528,38))
  CoreMonad.>>= (compiler/simplCore/CoreMonad.hs:(524,5)-(528,38))
  IOEnv.runIOEnv (compiler/utils/IOEnv.hs:127:1-30)
  CoreMonad.runCoreM (compiler/simplCore/CoreMonad.hs:(565,1)-(581,63))
  SimplCore.core2core (compiler/simplCore/SimplCore.hs:(75,1)-(99,54))
  HscTypes.liftIO.\ (compiler/main/HscTypes.hs:245:31-55)
  HscTypes.liftIO (compiler/main/HscTypes.hs:245:5-55)
  HscMain.Core2Core (compiler/main/HscMain.hs:1173:7-42)
  HscMain.hscSimplify' (compiler/main/HscMain.hs:(1170,1)-(1173,42))
  HscMain.finish (compiler/main/HscMain.hs:(702,1)-(740,70))
  HscTypes.>>=.\ (compiler/main/HscTypes.hs:(240,33)-(242,56))
  HscTypes.>>= (compiler/main/HscTypes.hs:(240,5)-(242,56))
  HscTypes.runHsc (compiler/main/HscTypes.hs:(251,1)-(254,12))
  HscMain.hscIncrementalCompile (compiler/main/HscMain.hs:(644,1)-(690,60))
  DriverPipeline.compileOne' (compiler/main/DriverPipeline.hs:(134,1)-(289,55))
  GhcMake.upsweep_mod.compile_it_discard_iface (compiler/main/GhcMake.hs:(1436,13)-(1438,61))
  GhcMake.upsweep_mod (compiler/main/GhcMake.hs:(1376,1)-(1532,49))
  GhcMonad.liftIO (compiler/main/GhcMonad.hs:110:3-30)
  GhcMake.upsweep.upsweep' (compiler/main/GhcMake.hs:(1245,3)-(1344,91))
  GhcMake.upsweep (compiler/main/GhcMake.hs:(1237,1)-(1344,91))
  GhcMake.load'.upsweep_fn (compiler/main/GhcMake.hs:(389,9)-(390,41))
  GhcMake.load' (compiler/main/GhcMake.hs:(242,1)-(490,38))
  GhcMake.load (compiler/main/GhcMake.hs:(234,1)-(236,44))
  Main.doMake (ghc/Main.hs:(695,1)-(720,13))
  GhcMonad.gcatch.\ (compiler/main/GhcMonad.hs:117:19-63)
  GhcMonad.gcatch (compiler/main/GhcMonad.hs:(116,3)-(117,63))
  ErrUtils.prettyPrintGhcErrors (compiler/main/ErrUtils.hs:(657,1)-(666,44))
  Main.main' (ghc/Main.hs:(154,1)-(258,33))
  GhcMonad.gmask.\.\.g_restore.\ (compiler/main/GhcMonad.hs:121:65-80)
  GhcMonad.gmask.\.\.g_restore (compiler/main/GhcMonad.hs:121:33-80)
  GhcMonad.gmask.\.\ (compiler/main/GhcMonad.hs:(120,30)-(123,53))
  Exception.gmask.\ (compiler/utils/Exception.hs:64:27-29)
  Exception.gmask (compiler/utils/Exception.hs:64:3-30)
  GhcMonad.gmask.\ (compiler/main/GhcMonad.hs:(119,19)-(123,53))
  GhcMonad.gmask (compiler/main/GhcMonad.hs:(118,3)-(123,53))
  Exception.gfinally (compiler/utils/Exception.hs:(56,3)-(60,14))
  GhcMonad.>>=.\ (compiler/main/GhcMonad.hs:107:26-57)
  GhcMonad.>>= (compiler/main/GhcMonad.hs:107:3-57)
  Panic.withSignalHandlers (compiler/utils/Panic.hs:(240,1)-(298,37))
  GHC.runGhc (compiler/main/GHC.hs:(440,1)-(445,26))
  Exception.gcatch (compiler/utils/Exception.hs:63:3-37)
  Exception.ghandle (compiler/utils/Exception.hs:73:1-21)
  GHC.defaultErrorHandler (compiler/main/GHC.hs:(380,1)-(412,7))
  Main.main (ghc/Main.hs:(90,1)-(150,64))

comment:4 Changed 2 years ago by goldfire

comment:3 is easy to diagnose: note that the stack includes substCoWithUnchecked, but the "uncheckedness" doesn't propagate. Not sure what the best way to fix this is, but the underlying problem is not ours.

comment:2 is as you describe: the inst_tvs here do not need to contain the kinds. But the InScopeSet surely does! Use closeOverKinds. This is a latent bug, as I expected.

comment:5 Changed 2 years ago by RyanGlScott

  • comment:2: Sorry, I shouldn't have used this example, since it's not actually tripping up the ASSERT. In fact, it does close over the kinds of the type variables, which you can see by looking at the definition of zipTvSubst:
zipTvSubst :: [TyVar] -> [Type] -> TCvSubst
zipTvSubst tvs tys
  | debugIsOn
  , not (all isTyVar tvs) || neLength tvs tys
  = pprTrace "zipTvSubst" (ppr tvs $$ ppr tys) emptyTCvSubst
  | otherwise
  = mkTvSubst (mkInScopeSet (tyCoVarsOfTypes tys)) tenv
  where
    tenv = zipTyEnv tvs tys

It uses tyCoVarsOfTypes to get the tyvars for the in-scope set, so they will include the necessary kind variables. Phew.

  • comment:3. Aha! What I should have done is split substTyVar into a checked version and an unchecked version, and use the unchecked version in subst_ty (subst_ty is already using substTyVarBndrUnchecked here, so this doesn't make things any less palatable than before).

I'll post an update after I've ran ./validate with this change.

comment:6 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3732
Status: newpatch

Happily, it passes ./validate! I also ran ./validate --slow, and I couldn't observe any additional ASSERT failures from this change (there were some ASSERT failures related to the substitution invariant before and after this chance, but importantly, the number of them remain unchanged with this patch).

Since I'm convinced this will just work, I've submitted Phab:D3732 to Phab.

comment:7 Changed 2 years ago by simonpj

I differ right at the start!

If you look at the corresponding code for term variables you'll see (in CoreSubst):

lookupIdSubst :: SDoc -> Subst -> Id -> CoreExpr
lookupIdSubst doc (Subst in_scope ids _ _) v
  | not (isLocalId v) = Var v
  | Just e  <- lookupVarEnv ids       v = e
  | Just v' <- lookupInScope in_scope v = Var v'
        -- Vital! See Note [Extending the Subst]
  | otherwise = WARN( True, text "CoreSubst.lookupIdSubst" <+> doc <+> ppr v
                            $$ ppr in_scope)
                Var v

We do not apply the substition to the type of the Id and update its type! Rather, we just look it up in the in-scope set: that should include all in-scope Ids; and moreover they are all full-substituted OutIds. A consequence is that all occurrences of the Id are common'd up to point to a single Id data structure, rather than having lots of copies of the Id.

We should do the same for types. In substTyVar, if the var isn't in the tenv look in the in-scope set. It should be there.

Of course, because we have not yet made all calls to substTy have the right in-scope set, we may not find it in the in-scope set. I suppose we can emit a warning, or just silently accept (as of course we are doing right now). Once we've fixed all the calls to substTy we should definitely make it a warning.

So it's an easy fix.

Did you say you'd found other lurking bugs as a result?

comment:8 Changed 2 years ago by goldfire

Who arranges for the members of the in-scope set to have substituted kinds? It's not uncommon to start a substitution with some in-scope set (derived from a call to tyCoVarsOfTypes or similar) and then build it from there. No one touches the in-scope set.

comment:9 Changed 2 years ago by simonpj

Who arranges for the members of the in-scope set to have substituted kinds?

Well, if the in-scope set comes from the context (as in the simplifier or other places) all the Vars in the in-scope set are OutIds; that is, fully substituted. It would be wrong to substitute again, because it's entirely OK to have a substitution that goes a :-> [a], because the LHS is InVars and the RHS is OutVaers. (This is not true during unification of course, but that's entirely separate.)

E.g. a substitution [a :-> Proxy k (b::k), k :-> *] really means "replace a by Proxy k (b::k)" and NOT "then apply the subsituton to the result to get Proxy * (b::*). No no no. Substitutions apply exactly once.

(In this example the k in Proxy k (b::k) is an OutTyVar whereas the k in k :-> * is an InTyVar.)

What if we build the in-scope set by taking the free vars of the range of the substitution? Eg.

Substitute  [a :-> Proxy k (b::k)]
in the type (a, b)

The in-scope set, from the range of the substitution, is {b,k}. Do we need to apply the substitution to {b}? No! The range of the substitution is OutVars so we must not apply the substitution to it.

A more delicate point is this: what if we build (part of) the in-scope set by taking the free vars of the type being substituted (see substTyAddInScope and Note [The substitution invariant] inTyCoRep? That's an InType! eg

Substitute  [a :-> Int]
in the type (a, b::k)

Now we get an in-scope set of {b::k}. But although b appears in an InType, it must be an OutTyVar precisely because it is not substituted. It must be bound somewhere outside, and it'd be wrong to substitute its kind at one of its occurrences and not at its binding site!

So I think everything is fine. But I really wish I had a clearer way to explain WHY it is fine.

comment:10 Changed 2 years ago by goldfire

After a long debate, Simon and I came up with the following claim:

(*) Claim: If a tyvar is not in the domain of a substitution, then no variables in its kind are in the domain of a substitution.

If (*) is true, then the change Phab:D3732 should be a no-op: precisely no behavior should change. And we can check (*) on the fly, which we should.

Why should (*) be true? Here's some rough reasoning: a tyvar a whose kind mentions k must be bound in k's scope. If we are substituting k (to Type, say), then we'll need to substitute both in a's binding site and a's scope. When we subst in the binding site (with substTyVarBndr), the subst is extended mapping a:k to a:Type; a is thus in the domain of the subst when we get to substing in a's scope. If we've forgotten to call substTyVarBndr, then we're in deep trouble, anyway. Thus, all tyvars whose kinds mention k will be added to the subst by the time we get to their scope.

But thinking about (*) led us to ponder this strange scenario: forall k. forall (b :: k). forall k. forall (a :: k). Proxy [a,b]. Is that well-kinded? Surely not, because a and b have different kinds: a's kind is the more local k while b's kind is the less local k. However, Core Lint is going to have a hard time with this. When Lint looks at [a,b], it will ask for a's kind and get k. It will ask for b's kind and get k. And the ks will be equal! Core Lint will accept. This is horrible. This bug may have been lurking in GHC for ages.

The remedy: don't do this. Specifically, we introduce

(+) Rule: When a tyvar a is brought into scope, all vars (type and term) whose type mentions a fall out of scope.

Under (+), b is not in scope in [a,b] and we have a straightforward scoping error. We can check this in Lint. We couldn't quite convince ourselves that (+) is actually always respected during transformations, etc., but by adding a rule in Lint, we can discover when it doesn't. An alternative to (+) is

(-) Rule: It is illegal to shadow a variable. That is, if a is in scope, we cannot bind a.

(-) implies (+) and is easy to check for. However, it may not be so easy to uphold; Simon claims several places in GHC knowingly violate (-), and avoiding this violation may hurt performance. I'm worried that any code that violates (-) will sometimes fall afoul of (+) (but only in very obscure scenarios). Simon claims that the violations of (-) but not (+) involve closed types and therefore are safe w.r.t. (+). So we've agreed to check for (+) for now and see how that goes.

As a sidenote: comment:7 and comment:9 concern term-level substitutions. At the term level, we have a real interest in commoning up occurrences (so that all occurrences of an Id x actually point to the same heap object) because of IdInfo. In types, on the other hand, we have an interest in avoiding forcing a TCvSubst's InScopeSet, and so we don't use the same "look up in in-scope set" approach. So, essentially, comment:7 and comment:9 are red herrings.

Bottom line

We have these tasks:

  1. Check for (*) in substTyVar. This is instead of the kind substitution discussed earlier in this ticket. Document (*).
  1. Update Core Lint to check (+). Document (+) in a nice Note.
  1. (Optional) If we blindly set no_kind_change to False in substTyVarBndrCallback, then substitutions will common up type variables by looking up type variables in the substitution. There's a chance this will have a performance benefit. Try and investigate.

comment:11 Changed 2 years ago by simonpj

Just to add: Rule (+) means that the following program is illegal:

forall (k:*). forall (a:k).
   forall (k:*->*).
      a

Note the shadowing: there are really two k's. It's illegal according to (+) because bringing the inner k into scope makes a (as well as the outer k) fall out of scope, because a's kind mentions k.

Why this rule? Because in the implementation we have kinds on every variable occurrence, and the kind on an occurrence should match that on the binder. So

forall (a:*).  (a:*) -> Int

is fine, but

forall (a:*). T (a:*->*)

is not, because the kind on a's occurrence doesn't match that at its binding site. And Rule (+) makes this illegal too:

forall (k:*). forall (a:k).
   forall (k:*->*).
      (a:k)

because the kind at a's occurrence is a different k to that at its binding site.

Another way to say it is that typeKind (and exprType) yield sane results.

comment:12 Changed 2 years ago by RyanGlScott

Differential Rev(s): Phab:D3732

Removing abandoned Diff.

comment:13 Changed 2 years ago by RyanGlScott

Status: patchnew

comment:14 Changed 2 years ago by goldfire

Ryan, are you working on this? Or should I add it to my queue? Or does Simon want it?

comment:15 in reply to:  14 Changed 2 years ago by RyanGlScott

Replying to goldfire:

Ryan, are you working on this?

No.

comment:16 Changed 2 years ago by simonpj

I'm not. Do add it to your queue, Richard. Thanks!

comment:17 Changed 2 years ago by goldfire

Owner: set to goldfire
Note: See TracTickets for help on using tickets.