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,321
    • Issues 4,321
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 359
    • Merge Requests 359
  • 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
  • #17395

Closed
Open
Opened Oct 23, 2019 by Simon Peyton Jones@simonpjDeveloper

`tcMatchTy` is terribly broken

Suppose (T :: forall k. k -> Type) and we are matching

   tcMatchTy (T k (a::k))  (T j (b::j))

Then we'll match k :-> j, as expected. But then in TcUnify.unify_tys we invoke

   unify_tys env (a::k) (b::j) (Refl k)

Despite Note [Kind coercions in Unify] it's not clear to me why we need that Refl coercion.

But, assuming we need it, very very bad things now happen. In uUnrefined we end up adding the binding a :-> (b |> Refl k).

Alas! Alack! k is one of the template variables, which we are substituting away, so it's terrible if k appears in the range of the substitution -- it belongs only in the range.

A one-line (actually one-character) fix is this:

-      = do { unify_ty env x y (mkNomReflCo $ typeKind x)
+      = do { unify_ty env x y (mkNomReflCo $ typeKind y)

But I am hard-pressed to explain exactly why this is the correct fix.

@rae, help?

This actually bit me when working on mkCastTy in #17323.

Assignee
Assign to
8.10.1
Milestone
8.10.1 (Past due)
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#17395