`substTm` mixes up term and type vars

[martijnbastiaan]

Consider two variables. One is a term variable:

termVar :: Var Term
termVar = Id {
    varName = fakeName {nameUniq=unique, nameOcc="term"}
  , varUniq = unique
  , varType = ConstTy (TyCon fakeName)
  , idScope = LocalId
  }

and the other a type variable

typeVar :: Var Type
typeVar = TyVar {
    varName = fakeName {nameUniq=unique, nameOcc="type"}
  , varUniq = unique
  , varType = ConstTy (TyCon fakeName)
  }

We'd expect that deshadowing Var termVar with an inScopeSet of just typeVar should be a no-op, as their uniques live in different name spaces. (In fact, it's not even possible to have both termVar and typeVar in an InScopeSet, as it only stores uniques!). deShadowTerm currently behaves differently though:

>>> deShadowTerm (extendInScopeSet emptyInScopeSet typeVar) (Var termVar)
Var (TyVar {varName = Name {nameSort = User, nameOcc = "type", nameUniq = 20, nameLoc = UnhelpfulSpan "<no location info>"}, varUniq = 20, varType = ConstTy (TyCon (Name {nameSort = User, nameOcc = "fake", nameUniq = 0, nameLoc = UnhelpfulSpan "<no location info>"}))})

instead of:

>>> deShadowTerm (extendInScopeSet emptyInScopeSet typeVar) (Var termVar)
Var (Id {varName = Name {nameSort = User, nameOcc = "term", nameUniq = 20, nameLoc = UnhelpfulSpan "<no location info>"}, varUniq = 20, varType = ConstTy (TyCon (Name {nameSort = User, nameOcc = "fake", nameUniq = 0, nameLoc = UnhelpfulSpan "<no location info>"})), idScope = LocalId})

The culprit seems to be anti space-leak measures in lookupIdSubst:

clash-compiler/clash-lib/src/Clash/Core/Subst.hs

Line 512 in a009fe4

| Just v' <- lookupInScope inScope v = Var (coerce v')

It should refuse to substitute TyVars with Ids.

[christiaanb]

The situation you describe though is really weird though. I have no idea how you end up in a situation where you have a free term variable with a type variable with the same unique in scope...

[martijnbastiaan]

It's specific to caseCon, where we add the existential vars to the inscopeset and then do a deshadow. We can probably leave that out, but I'm much more comfortable with just fixing substitution instead.

[christiaanb]

No, you should extend the inScopeSet. However, now I get what's going on, from substTms point-of-view we have built up an "ill-formed" inScopeSet. The reason that it's "ill-formed" is the original purpose of that inScopeSet was just to pick new variable names that were not in-scope, but not to be used within a substitution (which is what deShadowTerm does). I say "ill-formed" because substTm expects that any shadowing variable exists in the substitution environment, but we don't rename bound variables as we traverse down the expression during normalization and only keep an inscopeset around.

To explain what's going on, when we do:

deshadowTerm emptyInScopeSet (\x:Int . /\x:Type . x)

we get:

\x:Int . /\y:Type . x

however, during normalisation, we only extend/overwrite the inScopeSet.

and so when we traverse down the term, and call deShadowTerm on the variable reference, we get:

deShadowTm {x:Type} x

i.e. the x:Type will have overwritten the x:Int of the inScopeSet.
@martijnbastiaan Could you add something along the above in the comments, perhaps as a Note, to your patch?