I am quite comfortable with Agda. I decided to experiment with Lean, but I find that propositional equality is really messing with me. Sometimes I find that rfl just works, but at other times it doesn't for reasons that totally escape me, which is rather frustrating. To give an example:
inductive Λ where
| var : String → Λ
| app : Λ → Λ → Λ
| abs : String → Λ → Λ
deriving Repr, BEq, DecidableEq
def FV : Λ → HashSet String
| Λ.var x => HashSet.ofList [x]
| Λ.app m n => FV m ∪ FV n
| Λ.abs x m => (FV m).erase x
#eval FV (Λ.var "x") -- Std.HashSet.ofList ["x"]
example : FV (Λ.var "x") = HashSet.ofList ["x"] := rfl -- fine
example : (2 == 1 + 1) = true := rfl -- fine
#eval FV (Λ.var "x") == HashSet.ofList ["x"] -- true
example : (FV (Λ.var "x") == HashSet.ofList ["x"]) = true := rfl
--type mismatch
-- rfl
--has type
-- ?m.9390 = ?m.9390 : Prop
--but is expected to have type
-- (FV (Λ.var "x") == HashSet.ofList ["x"]) = true : Prop
The expressions evaluate as expected, but in the first two examples, rfl works just fine, but in the last it mysteriously doesn't, seemingly not reducing the terms on both sides of the = . I could imagine two HashSets with the same values not always being equal as they might have ended up in different buckets, but I am not sure if that is the issue, because it seems to evaluate just fine.
The issue here is not so much with the equality type, as the fact that #eval is not the same as kernel reduction, and many complex definitions are done in such a way that while they have good computational properties (in the sense of producing efficient code), they don't reduce in the kernel well or at all. One of the main causes for this is that the definition depends in some way on well founded recursion, which is usually marked as irreducible and hence will block kernel computation. In this case I would be suspecting the HashSet.ofList function and the == function on HashSet as being the reason for this to fail to compute in the kernel.