Equation solver behavior inconsistency

[ice1000]

This code checks:

\func M : \Pi (x : S1) -> \Type => \lam x => \case x \with {
   | base => I
   | loop i => twist @ i
}

But this doesn't:

\func M (x : S1) : \Type
   | base => I
   | loop i => twist @ i

Error:

Cannot solve equations   \lh = \oo

[valis]

This is an expected behavior because the type of a function defined by pattern matching is checked before the body, but the type of the first version is checked together with the body.

[valis]

Actually, we can defer the inference of levels for the type in the second version.