Skip to content

GitLab

  • Projects
  • Groups
  • Snippets
  • Help
    • Loading...
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
GHC
GHC
  • Project overview
    • Project overview
    • Details
    • Activity
    • Releases
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 4,262
    • Issues 4,262
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 419
    • Merge Requests 419
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
  • Security & Compliance
    • Security & Compliance
    • Dependency List
    • License Compliance
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Collapse sidebar
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #11371

Closed
Open
Opened Jan 07, 2016 by Simon Peyton Jones@simonpjDeveloper

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
Assignee
Assign to
8.4.1
Milestone
8.4.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#11371