reduce needs for InScopeSets?

[Simon Peyton Jones]

It's _nothing_ to do with whether the kind changes!

It's everything to do with cloning the binder if it is already in scope.  See "Secrets of the GHC inliner", the section called "The rapier", I think.

| Separately, I also see that substTyVar does not currently recur into a
| tyvar's kind, if the tyvar is not mapped by the substitution. This behavior
| seems wrong to me, but I guess it's worked thus far.

Well that would be deeply strange.  The point is that every occurrence of a type variable should have the same kind as its binding site.  So if we have
    forall (a:k).  ....(a:k')....
then k and k' should jolly well be the same.

Suppose the substitution S has a binding kv -> k, for some kind variable kv.  Then suppose apply this substitution to 
    forall (a:blah). ...(a:blah)...
where blah mentions kv. Then we'll substitute k for kv in blah, and extend the substitution with (a:blah) -> (a : S(blah)). That will ensure that all occurrences of a get updated.

But it would be most odd to apply S to the body of the forall, but not to the binder.   Recursing into the kind would give 
   forall (a:blah. ....(a:S(blah))...
which is bogus (Lint will reject it).  But not recursing into the kind would also go wrong if we had, say (Proxy blah (a:blah)).  The if we don’t recurse in we'd get Proxy S(blah) (a:blah), which is bogus.

So there's another invariant hiding here, but I'm not sure how to state it.

Simon
  
| -----Original Message-----
| From: ghc-devs [mailto:ghc-devs-bounces at haskell.org] On Behalf Of Richard
| Eisenberg
| Sent: 11 April 2016 20:53
| To: ghc-devs at haskell.org developers <ghc-devs at haskell.org>
| Subject: reduce needs for InScopeSets?
| 
| Hi all,
| 
| I now frequently run across ASSERTion failures triggered by the new
| substitution invariant checks. This is surely a good thing, but it's gotten
| me thinking about the need for InScopeSets in substitutions at all. It seems
| to me that the only(?) use of the InScopeSet is in the uniqAway in
| substTyVarBndr. uniqAway is used here when the kind of a tyvar changes.
| 	
| Why do we need a new unique when a tyvar's kind changes? Can't we just update
| the kinds of tyvar occurrences?
| 
| One might argue that updating tyvar occurrences' kinds is inefficient. This
| may be true, but we can tackle that problem head-on by storing a separate
| TyVarEnv Type that contains tyvar occurrence updates. There's still no need
| for a new unique.
| 
| If we can get rid of InScopeSets in substitutions, that would be a wonderful
| thing, I think.
| 
| Separately, I also see that substTyVar does not currently recur into a
| tyvar's kind, if the tyvar is not mapped by the substitution. This behavior
| seems wrong to me, but I guess it's worked thus far.
| 
| Thoughts?
| 
| Richard
| _______________________________________________
| ghc-devs mailing list
| ghc-devs at haskell.org
| http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs