diff --git a/library/init/lean/typeclass/context.lean b/library/init/lean/typeclass/context.lean index cdf472d70d..4d0d3affb5 100644 --- a/library/init/lean/typeclass/context.lean +++ b/library/init/lean/typeclass/context.lean @@ -190,7 +190,7 @@ partial def slowWhnf : Expr → Expr partial def eUnify : Expr → Expr → EState String Context Unit | e₁, e₂ => if !e₁.hasMVar && !e₂.hasMVar - then unless (e₁ == e₂) $ throw "fail" + then unless (e₁ == e₂) $ throw $ "eUnify: " ++ toString e₁ ++ " !=?= " ++ toString e₂ else do e₁ ← slowWhnf <$> (EState.fromState $ eShallowInstantiate e₁); e₂ ← slowWhnf <$> (EState.fromState $ eShallowInstantiate e₂); diff --git a/tests/lean/typeclass_context.lean.expected.out b/tests/lean/typeclass_context.lean.expected.out index 11ff2b768d..296cdbea95 100644 --- a/tests/lean/typeclass_context.lean.expected.out +++ b/tests/lean/typeclass_context.lean.expected.out @@ -7,8 +7,8 @@ (ok foo) (ok f a) (error "eUnify: f !=?= g") -(error "eUnify: f !=?= g") -(error "eUnify: a !=?= b") +(error "eUnify: f a !=?= g a") +(error "eUnify: f a !=?= f b") (error "eUnify: f a !=?= f") (ok foo) (ok f ?_tc_alpha.0 ?_tc_alpha.1)