Don't constraint template polymorphic universes of list and option redefining `MBind` and related typeclasses
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
Merge request reports
Activity
- Resolved by Michael Sammler
Robbert mentioned this as a possibility to me yesterday, but this seems like it would be really bad for type inference.
CI passes though, so it can't break it completely. I have triggered reverse dependency CI builds.
- Resolved by Michael Sammler
Iris itself already fails to build, though it's not about type inference:
# COQC iris/proofmode/intro_patterns.v # File "./iris/algebra/ofe.v", line 1301, characters 61-67: # Error: # In environment # A : ofe # B : ofe # n : nat # The term "option" has type "Type → Type" while it is expected to have type # "Type". # # make[1]: *** [Makefile.package.iris:832: iris/algebra/ofe.vo] Error 1
mentioned in commit iris@fbf28bc1
mentioned in merge request iris!1050 (merged)
- Resolved by Robbert Krebbers
Does this fix #207 ?
- Resolved by Robbert Krebbers
One additional remark about this is that it allows to implement
MBind'
forgset
like:Global Instance gset_bind : ∀ `{Countable A} `{Countable B}, MBind' A (gset A) (gset B) Admitted.
Probably can do that on other type-classes too
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. changed this line in version 10 of the diff
added 1 commit
- 21e36706 - Avoid constraining template polymorphic types
- Resolved by Robbert Krebbers
- Resolved by Michael Sammler
- Resolved by Michael Sammler
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
andFinMap
, but they are a bit harder to solver.- Resolved by Michael Sammler
added 1 commit
- 6a824e2f - Avoid constraining template polymorphic types
mentioned in commit iris@79129170
added 1 commit
- f72d514c - Avoid constraining template polymorphic types
mentioned in commit iris@8e4b09ee
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