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
From HB RequireImport structures.
HB.mixin Record hasPoint T := { point : T }.
HB.structure Definition Pointed := { T of hasPoint T }.
Definition image_type {T} {iT} (f : T -> iT) := iT.
Fail HB.instance Definition _ (pT : Pointed.type) iT f :=
hasPoint.Build (image_type f) (f point).
fails with error message
Unification problem outside the pattern fragment. ((Data.Term.AppUVar ([...])))
instead of either inferring f or saying it should be explicitly annotated.
The text was updated successfully, but these errors were encountered:
If the inference worked it would rely both on image_type and point though... (for a complete inference), and neither occur in the error message. How is it relevant?
fails with error message
instead of either inferring
f
or saying it should be explicitly annotated.The text was updated successfully, but these errors were encountered: