5da7f0b50b
We don't want contraints such as ``` ?m a =?= Nat ``` to be solved as ``` ?m := fun a => Nat ``` durint type class resolution.
18 lines
502 B
Text
18 lines
502 B
Text
phashmap_inst_coherence.lean:12:6: error: application type mismatch
|
|
Std.PersistentHashMap.find? m
|
|
argument
|
|
m
|
|
has type
|
|
Std.PersistentHashMap Nat Nat
|
|
but is expected to have type
|
|
Std.PersistentHashMap Nat Nat
|
|
failed to synthesize instance
|
|
CoeT (Std.PersistentHashMap Nat Nat) m (Std.PersistentHashMap Nat Nat)
|
|
phashmap_inst_coherence.lean:12:0: error: application type mismatch
|
|
Lean.runEval (sorryAx ?m.307)
|
|
argument
|
|
(sorryAx ?m.307)
|
|
has type
|
|
?m.307
|
|
but is expected to have type
|
|
?m.309
|