parenthesize for CornelisSolve

[leo-leesco]

I noticed that when I use CornelisSolve (most of the time) the result that is inputted automatically is not parenthesized. An example of such behaviour can be found in a course-lab I was working on.

Situation :

isPropIsOfHLevel : {A : Type ℓ} (n : HLevel) → isProp (isOfHLevel n A)
isPropIsOfHLevel zero = isPropIsContr
isPropIsOfHLevel (suc n) p q = funExt λ { x → funExt λ { y → isPropIsOfHLevel n (p x y) {!q !} } }

Expected result :

isPropIsOfHLevel : {A : Type ℓ} (n : HLevel) → isProp (isOfHLevel n A)
isPropIsOfHLevel zero = isPropIsContr
isPropIsOfHLevel (suc n) p q = funExt λ { x → funExt λ { y → isPropIsOfHLevel n (p x y) (q x y) } }

Actual result :

isPropIsOfHLevel : {A : Type ℓ} (n : HLevel) → isProp (isOfHLevel n A)
isPropIsOfHLevel zero = isPropIsContr
isPropIsOfHLevel (suc n) p q = funExt λ { x → funExt λ { y → isPropIsOfHLevel n (p x y) q x y } }

And rightfully enough, Agda complains about that because it is ill-typed…

I know just about nothing regarding Haskell, so :

• the few lines I added might be outright antipatterns
• I'd be very happy if you could help me improve/explain a little what is the correct mechanism to handle what I did (or if there is any)
• if this was the right thing to do, maybe explain if there should have been a better way to write that ?

Anyway, it seems like this fixes the bug, I'm not sure it did not introduce any other.
Best,
Léo
PS: btw, thank you for this absolute of a banger of a plugin. I mean it, it's absolutely great ! Apart from this little inconvenience, it's more or less perfect

[4e554c4c]

just to double check: i do some parenthesizing in #187
does that fix the problem?