Skip to content
Snippets Groups Projects

Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses

Open Michael Sammler requested to merge msammler/monad_without_universe_constraints into master

This is an idea how to fix #80 and #207 . Since M never appears unapplied, it should not introduce the universe constraints. Note that the universe of gmap and gset and similar remain constrained due to the MonadSet and FinMap typeclasses.

In particular, with

Class MBind (M : Type → Type) := mbind : ∀ {A B}, (A → M B) → M A → M B.
Global Instance x : MBind list.
Admitted.
Print Universes.

one gets the contraint list.u0 = MBind.u0. But with

Class MBind' (A MA MB : Type) := mbind : (A → MB) → MA → MB.
Notation MBind M := (∀ A B, MBind' A (M A) (M B)).
Global Instance x : MBind list.
Admitted.
Print Universes.

one only gets the constraints

x.u0 <= list.u0
x.u0 <= MBind'.u0
x.u0 <= MBind'.u1
x.u1 <= list.u0
x.u1 <= MBind'.u2
Edited by Michael Sammler

Merge request reports

Merge request pipeline #115640 passed

Merge request pipeline passed for a0812a62

Ready to merge by members who can write to the target branch.
Loading

Activity

Filter activity
  • Approvals
  • Assignees & reviewers
  • Comments (from bots)
  • Comments (from users)
  • Commits & branches
  • Edits
  • Labels
  • Lock status
  • Mentions
  • Merge request status
  • Tracking
1199 1199 Global Instance: Params (@mret) 3 := {}.
1200 1200 Global Hint Mode MRet ! : typeclass_instances.
1201 1201
1202 Class MBind (M : Type Type) := mbind : {A B}, (A M B) M A M B.
1202 Class MBind' (A MA MB : Type) := mbind : (A MB) MA MB.
1203 Notation MBind M := ( A B, MBind' A (M A) (M B)).
1203 1204 Global Arguments mbind {_ _ _ _} _ !_ / : assert.
1204 1205 Global Instance: Params (@mbind) 4 := {}.
1205 Global Hint Mode MBind ! : typeclass_instances.
1206 Global Hint Mode MBind' - - ! : typeclass_instances.
  • added 1 commit

    • 21e36706 - Avoid constraining template polymorphic types

    Compare with previous version

  • From discussion with @robbertkrebbers : The plan for this MR is to solve the universe problem for list and option. There are more universe problems coming from MonadSet and FinMap, but they are a bit harder to solver.

  • Ralf Jung
  • added 1 commit

    • 6a824e2f - Avoid constraining template polymorphic types

    Compare with previous version

  • mentioned in commit iris@79129170

  • added 1 commit

    • f72d514c - Avoid constraining template polymorphic types

    Compare with previous version

  • mentioned in commit iris@8e4b09ee

  • Michael Sammler marked this merge request as ready

    marked this merge request as ready

  • Michael Sammler changed title from Draft: Attempt at defining a version of MBind that does not impose universe constraints to {+Solve #207 by redefining MBind and related typeclasse+}s

    changed title from Draft: Attempt at defining a version of MBind that does not impose universe constraints to {+Solve #207 by redefining MBind and related typeclasse+}s

  • Michael Sammler changed the description

    changed the description

  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Loading
  • Please register or sign in to reply
    Loading