fix(typeclass/context): standardize eUnify fail message

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₂);

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)