Skip to content

GitLab

  • Menu
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 4,866
    • Issues 4,866
    • List
    • Boards
    • Service Desk
    • Milestones
    • Iterations
  • Merge requests 461
    • Merge requests 461
  • 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 Compiler
  • GHCGHC
  • Issues
  • #17201
Closed
Open
Created Sep 17, 2019 by Krzysztof Gogolewski@monoidalDeveloper

Levity polymorphism and defaulting

This ticket concerns two closely related items regarding levity polymorphism.

  1. Consider
f1 :: forall (p :: RuntimeRep -> Type) (r :: RuntimeRep). p r -> p r
f1 x = x

-- Inferred type g1 :: forall (p :: RuntimeRep -> Type). p 'LiftedRep -> p 'LiftedRep
g1 = f1

f2 :: (p :: Bool -> Type) (r :: Bool). p r -> p r
f2 x = x

-- Inferred type g2 :: forall (p :: Bool -> Type) (r :: Bool). p r -> p r
g2 = f2

f3 :: forall k (p :: k -> Type) (r :: k). p r -> p r
f3 x = x

-- Inferred type g3 :: forall k (p :: k -> Type) (r :: k). p r -> p r
g3 = f3

type family R
type instance R = RuntimeRep
f4 :: (p :: R-> Type) (r :: R). p r -> p r
f2 x = x

-- Inferred type g4 :: forall (p :: R -> Type) (r :: R). p r -> p r
g4 = f4

As you can see g1 gets a less general type than g2, but the only difference is RuntimeRep vs Bool.

And g3 also gets a more general type, even though k could be instantiated to RuntimeRep in a call.

And g4 disguises RuntimeRep behind a type family, and so becomes polymorphic.

This inconsistency is all pretty disgusting.

Proposed alternative:

  • When we typecheck a binder, we unify the kind of its type with TYPE q, and emit a new constraint StaticRuntimeRep q. Similarly for other places where levity polymorphsm
  • Never generalise over StaticRuntimeRep constraints.
  • Default any unsolved StaticRuntimeRep constraints at the end.

That could even be connected the defaulting mechanism, so that you could say default (UnliftedRep) in a module, or default (One) for multiplicity polymorphism in linear types.

Richard says that a lot of machinery for TypeLike (#15979) will overlap with this ticket.

  1. Consider
f x = x
g = f 0#

Currently, when f is typechecked, it's argument is inferred to be lifted, and typechecking of g fails. An alternative strategy is to mimic monomorphism restriction. Rather than defaulting RuntimeRep varaibles in TcMType.defaultTyVar, simply refrain from quantifying over it. The type of f would be forall (a :: TYPE q). a -> a, where q is a free unification variable.

Edited Jul 06, 2020 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