checkSolution, should meta solution be checked?

[atennapel]

In checkSolution (

elaboration-zoo/03-holes/Main.hs

Line 335 in 91e39dc

Meta m' -> when (m == m') $

) the type to be checked is quoted but the meta solutions are not inlined (no zonking). That makes the assumption that all meta solution in the type are valid for the meta we are trying to solve. Is this assumption valid?

[AndrasKovacs]

Metas are unfolded in quoting. The force does it in this line.

[atennapel]

Aah of course, thanks.