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,390
    • Issues 4,390
    • List
    • Boards
    • Labels
    • Service Desk
    • Milestones
    • Iterations
  • Merge Requests 373
    • Merge Requests 373
  • Requirements
    • Requirements
    • List
  • CI / CD
    • CI / CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Operations
    • Operations
    • Incidents
    • Environments
  • Analytics
    • Analytics
    • CI / CD
    • Code Review
    • Insights
    • Issue
    • Repository
    • Value Stream
  • Wiki
    • Wiki
  • Snippets
    • Snippets
  • Members
    • Members
  • Activity
  • Graph
  • Create a new issue
  • Jobs
  • Commits
  • Issue Boards
Collapse sidebar
  • Glasgow Haskell Compiler
  • GHCGHC
  • Issues
  • #17790

Closed
Open
Opened Feb 05, 2020 by Richard Eisenberg@raeDeveloper

`case` needn't instantiate its scrutinee

Consider

foo = case id of id' -> (id' 'x', id' True)

Should this be accepted or rejected? GHC currently rejects. But simply by changing this line to use tcInferSigma instead of tcInferRho, the program is accepted. (That's really it! Try it at home!)

Should we make this change? It makes our language more expressive. It also gets us closer to the Platonic ideal of a Hindley-Milner language design, in that users should never have to think about instantiation or generalization. And ML does it. If I write

let ex = match fun x -> x with
           | f -> (f 'x', f true)

then ocamlc accepts without complaint. Actually, this ML example is even more interesting: not only does it preserve the polymorphism in the scrutinee, it actually generalizes. Really, if Damas and Milner had been examining a language with case, they would have said that we need generalization at let and at case.

Of course, we could use tcInferSigma (enabling the Haskell example) but not to generalization. That means that foo would be accepted, but this bar would be rejected:

bar = case \x -> x of id' -> (id' 'x', id' True)

That's a bit of a shame.

This ticket is to track this small design decision.

Assignee
Assign to
None
Milestone
None
Assign milestone
Time tracking
None
Due date
None
Reference: ghc/ghc#17790