Miscellaneous coercion fixes #1981
Conversation
| @@ -163,6 +163,7 @@ attribute [coe_decl] CoeOTC.coe | |||
|
|
|||
| instance [CoeOut α β] [CoeOTC β γ] : CoeOTC α γ where coe a := CoeOTC.coe (CoeOut.coe a : β) | |||
| instance [CoeTC α β] : CoeOTC α β where coe a := CoeTC.coe a | |||
| instance : CoeOTC α α where coe a := a | |||
There was a problem hiding this comment.
We already had the reflexivity instance for CoeTC, this just adds them for the other auxiliary classes as well.
| @@ -32,26 +32,18 @@ partial def expandCoe (e : Expr) : MetaM Expr := | |||
| return .visit e.headBeta | |||
| return .continue | |||
|
|
|||
| register_builtin_option maxCoeSize : Nat := { | |||
There was a problem hiding this comment.
I'm so done with these arbitrary limits. I spent an hour yesterday trying to figure out what broke with the latest update. Why CoeHTCT worked but CoeT didn't, etc.
There's no reason to have a limit here, and I'm not willing to waste any more time debugging the random breakage this causes.
| @@ -102,7 +102,7 @@ partial def normLevel (u : Level) : M Level := do | |||
| | Level.max v w => return u.updateMax! (← normLevel v) (← normLevel w) | |||
| | Level.imax v w => return u.updateIMax! (← normLevel v) (← normLevel w) | |||
| | Level.mvar mvarId => | |||
| if !(← isLevelMVarAssignable mvarId) then | |||
| if (← getMCtx).getLevelDepth mvarId != (← getMCtx).depth then | |||
There was a problem hiding this comment.
This was an oversight in #1953. The isLevelMVarAssignable used to check for depth equality, irrespective of whether ignoreLevelMVarDepth was set or not. (While other functions like isReadOnly took it into account.) Now these functions all use the same logic.
This is important when users plug custom instances into auxiliary classes like `CoeTC`. We already had a reflexivity instance for `CoeTC`.
|
Merging to unblock the mathlib bump. |
These are various fixes to get mathlib to compile again.