Skip to content
GitLab
Projects Groups Snippets
  • /
  • Help
    • Help
    • Support
    • Community forum
    • Submit feedback
  • Sign in / Register
  • GHC GHC
  • Project information
    • Project information
    • Activity
    • Labels
    • Members
  • Repository
    • Repository
    • Files
    • Commits
    • Branches
    • Tags
    • Contributors
    • Graph
    • Compare
    • Locked Files
  • Issues 5,249
    • Issues 5,249
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 573
    • Merge requests 573
  • CI/CD
    • CI/CD
    • Pipelines
    • Jobs
    • Schedules
    • Test Cases
  • Deployments
    • Deployments
    • Releases
  • Analytics
    • Analytics
    • Value stream
    • 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
  • #17567
Closed
Open
Issue created Dec 11, 2019 by Richard Eisenberg@raeDeveloper

Never `Any`-ify during kind inference

#14198 concludes with a new plan: never Any-ify during kind inference. This ticket tracks this particular problem, separate from #14198.

Here are some examples of Any-ification during kind inference:

#17301 (closed):

data B a

data TySing ty where
  SB :: TySing (B a)

data ATySing where
  MkATySing :: TySing ty -> ATySing

type family Forget ty :: ATySing where
  Forget (B a) = MkATySing SB

The RHS of that type family equation is really MkATySing @alpha (SB @alpha), and the alpha gets zonked to Any.

#14198:

type T = forall a. Proxy a

The RHS of the type synonym is really forall (a :: kappa). Proxy @kappa a, and the kappa gets zonked to Any.

#17562 (closed):

class (forall a. a b ~ a c) => C b c

The superclass constraint is really forall (a :: Type -> kappa). (~) @kappa (a b) (a c)), and the kappa gets zonked to Any.

We want to stop zonking to Any, preferring to error instead. But how should we implement?

  • Option A: Use a new variant of ZonkFlexi, a choice carried around in a ZonkEnv that says what to do with empty metavariables. The new choice would cause an error. This new form of ZonkFlexi would be used in the final zonks in e.g. TcTyClsDecls. Open question: how to get a decent error message? I think we'd have to pass around the original, top-level type in order to report it. By the time we have just the unbound metavariable, we have no context to report.

  • Option B: Similar to (A), but don't report an error in the zonker. Instead, the new variant of ZonkFlexi would insert some magical error type. Then, the validity checker could do an early pass, looking for the error type; it can then report a nice error message.

  • Option C: Look for all cases where Any-ification might happen, and detect each one separately. This can produce lovely error messages. The solution for #17562 (closed) in !2313 (closed) does this. Perhaps we can pair this choice with a new ZonkFlexi that panics. That way, we'll know if we've missed a case.

  • Simon below proposes Option D: Zap to Type instead of Any. I (Richard) view D as an add-on to any of the above plans. Because Type is not always well-kinded, we can only zap to Type sometimes, and we still need to decide what we do at other times. Personally, I prefer not to treat Type specially with -XPolyKinds` enabled, and so I'd prefer that we don't do this.

  • EDIT: Also, we can consider Option E: Report poor error messages, saying something about an unconstrained kind variable. Users would be helped only via the context (the "In the data declaration for Wurble" bits). This would mean building up useful contexts in the zonker.

  • Option F: The new constructor for ZonkFlexi could carry the top-level type we are trying to zonk. If we encounter an unconstrained metavariable, we just look at this bit of context to produce the error message. Perhaps this could be combined with the context-building in Option E for good effect. This is the first solution I'm actually happy with.

Thoughts?

Edited Dec 16, 2019 by Simon Peyton Jones
To upload designs, you'll need to enable LFS and have an admin enable hashed storage. More information
Assignee
Assign to
Time tracking