Unification should check for spine length equality?

[atennapel]

Shouldn't the spines be the same length here:

elaboration-zoo/03-holes/Main.hs

Line 396 in d89688a

(VNe h sp, VNe h' sp') | h == h' -> zipWithM_ (go vs) sp sp'

[AndrasKovacs]

The two sides in unification always have the same type, so if the heads are equal, then the spines cannot be of different length (because then the sides would have different type).

[atennapel]

Right, that makes sense.