Skip to content
GitLab
Projects Groups Topics Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Register
  • Sign in
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributor statistics
    • Graph
    • Compare revisions
    • Locked files
  • Issues 5.6k
    • Issues 5.6k
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 656
    • Merge requests 656
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Artifacts
    • Schedules
    • Test cases
  • Deployments
    • Deployments
    • Releases
  • Packages and registries
    • Packages and registries
    • Model experiments
  • Analytics
    • Analytics
    • CI/CD
    • Code review
    • Insights
    • Issue
    • Repository
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell CompilerGlasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11371

Bogus in-scope set in substitutions

Bartosz reports that substitution isn't working properly for him. He cites this Note in TyCoRep:

-- Note [Generating the in-scope set for a substitution]
-- ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-- If we want to substitute [a -> ty1, b -> ty2] I used to
-- think it was enough to generate an in-scope set that includes
-- fv(ty1,ty2).  But that's not enough; we really should also take the
-- free vars of the type we are substituting into!  Example:
--      (forall b. (a,b,x)) [a -> List b]
-- Then if we use the in-scope set {b}, there is a danger we will rename
-- the forall'd variable to 'x' by mistake, getting this:
--      (forall x. (List b, x, x))
-- Urk!  This means looking at all the calls to mkOpenTCvSubst....

I think this is an outright bug that has been lurking for ages, and which Bartosz has just managed to tickle.

Things to do:

  • We should add an ASSERT to substTy (and similar functions): when calling substTy subst ty it should be the case that the in-scope set in the substitution is a superset of both

    • The free vars of the range of the substitution
    • The free vars of ty minus the domain of the substitution

    That ASSERT could be added to the immediate callers of subst_ty in TyCoRep.

    (Bartosz: if you add that you should find that it trips before the bug you are actually getting.)

  • How to fix it properly? The places to look are: everywhere that uses (transitively) one of the mkOpenTCvSubst or zipOpenTCvSubst functions.

    • Many calls to mkOpenTCvSubst produce a substitution that is only applied to closed types; or at least to types whose only free variables are the ones in the domain of the substitution. Example: the call to zipOpenTCvSubst in DataCon.dataConInstSig. These ones will all satisfy the ASSERT.

    • In other cases, we already have the in-scope set in hand. Example: in CoreLint.lintTyApp we find a call to substTyWith. But Lint carries an in-scope set, so it would be easy to pass it to substTyWith.

    • Finally there may be cases where we really have to take the free vars of the type we are substituting into, and add them to the in-scope set.

Doubtless all this applies to substituting in coercions too, and indeed into expressions.

Edited Feb 14, 2020 by Ömer Sinan Ağacan
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking