Cover more unification codepaths in the testsuite

[brendanzab]

Some of the codepaths in unification are not currently covered by the testsuite.

• fathom/fathom/src/surface/elaboration/unification.rs

  Line 306 in b8e8b31

  return Err(Error::Mismatch);

  • f x = (f x).foo (spine lengths differ)

• fathom/fathom/src/surface/elaboration/unification.rs

  Line 314 in b8e8b31

  (_, _) => return Err(Error::Mismatch),

  • f x = f y(failed to unify arguments)
  • (f x).bar = (f x).foo(record projections labels differ)

• fathom/fathom/src/surface/elaboration/unification.rs

  Line 344 in b8e8b31

  return Err(Error::Mismatch);

  • probably can't trigger this code path at the moment with something like {} = { x : T }, as this is caught by early-check of labels0 != labels1

One attempt I had at making a test for the first codepath was:

let test_left : fun (f : Type -> { foo : Type }) -> fun (x : Type) -> f x -> (f x).foo = 
   fun _ => fun _ => fun x => x;

let test_right : fun (f : Type -> { foo : Type }) -> fun (x : Type) -> (f x).foo -> f x = 
   fun _ => fun _ => fun x => x;

Type

Alas, I don't think that this actually triggers conversion checking, so I'll have to think a bit more carefully about this.