#13959: substTyVar's definition is highly dubious -------------------------------------+------------------------------------- Reporter: RyanGlScott | Owner: (none) Type: bug | Status: patch Priority: normal | Milestone: Component: Compiler | Version: 8.0.1 Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3732 Wiki Page: | -------------------------------------+------------------------------------- Comment (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 `Var`s 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]` in`TyCoRep`? 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. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13959#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler