You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
In the presence of universe variables, tcresolve doesn't work. Consider the following module:
moduleBugclassfoo(t:Type0):Type={u:Type}// or this explicit version, same issue:// class foo (t: Type0): Type u#(max 1 (n+1)) = { u: Type u#n }letworks{|foou#m't|}:foou#m't=_by(FStar.Tactics.Typeclasses.tcresolve())[@expect_failure]letfails{|foo't|}:foo't=_by(FStar.Tactics.Typeclasses.tcresolve())
The uvars of the top-level fails are basically infered as:
In the presence of universe variables,
tcresolve
doesn't work. Consider the following module:The uvars of the top-level
fails
are basically infered as:Thus the goal is impossible to fill.
The text was updated successfully, but these errors were encountered: