Seemingly incorrect type printing on a specific case

[hyphenrf]

Hello, I've been playing with proofs that require function extensionality and came across this strange behaviour on the :t command: on 0.5.1-9ce990e81

record St s a where
  constructor Mks
  run : s -> (a, s)

interface Semigroup ty => SemigroupV ty where
  sassoc : {x,y,z : ty} -> (x <+> y) <+> z = x <+> (y <+> z)

Semigroup a => Semigroup (St s a) where
  (Mks f) <+> (Mks g) = Mks $ \s0 =>
    let (a1, s1) = g s0
        (a2, s2) = f s1
     in (a1 <+> a2, s2)

SemigroupV a => SemigroupV (St s a) where
  sassoc {x = Mks f} {y = Mks g} {z = Mks h} = ?help

trying :t help, the types seem incorrect the type prints as:

Mks (\s0 => let (a1, s1) = h s0 in let (a2, s2) = f s1 in (a1 <+> a2, s2)) = Mks (\s0 => let (a1, s1) = let (a1, s1) = h s0 in let (a2, s2) = f s1 in (a1 <+> a2, s2) in let (a2, s2) = f s1 in (a1 <+> a2, s2))

or prettified and with cong Mks:

( \s0 => let (a1, s1) = h s0 in
         let (a2, s2) = f s1 in
             (a1 <+> a2, s2) )
=
( \s0 => let (a1, s1) =
             let (a1, s1) = h s0 in
             let (a2, s2) = f s1 in
                 (a1 <+> a2, s2)
          in let (a2, s2) = f s1 in
                 (a1 <+> a2, s2) )

This seems incorrect. The expected type should include g and be two equal-sized expressions with different associativity.

Note: I'm fairly new to the language and the problem could be in my code. But it seems not. As reducing that type equation would result in:

(a1 <+> a2, s2) = (a1 <+> a2 <+> a2', s2')

[gallais]

Somewhat shrunk & we still get a lot of nonsense in the goal type:

interface Semigroup ty => SemigroupV ty where
  sassoc : {x,y,z : ty} -> (x <+> y) <+> z = x <+> (y <+> z)

data Wrap : Type -> Type where
  MkW : a -> Wrap a

Semigroup a => Semigroup (Wrap a) where
  f <+> g = MkW $
    let MkW a1 = g
        MkW a2 = f
     in a1 <+> a2

SemigroupV a => SemigroupV (Wrap a) where
  sassoc = ?help

IIRC a pattern-matching let is elaborated to a case and we know from e.g. #1282 that printing of case ... of can be pretty dubious.