T15370.hs:14:10: warning: [-Wdeferred-type-errors (in -Wdefault)]
    • Couldn't match type ‘n’ with ‘j’
      Expected: n :~: j
        Actual: n :~: n
      ‘n’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
        at T15370.hs:13:1-17
      ‘j’ is a rigid type variable bound by
        the type signature for:
          mkRefl :: forall {k} (n :: k) (j :: k). n :~: j
        at T15370.hs:13:1-17
    • In the expression: Refl
      In an equation for ‘mkRefl’: mkRefl = Refl
    • Relevant bindings include
        mkRefl :: n :~: j (bound at T15370.hs:14:1)

T15370.hs:20:13: warning: [-Wdeferred-type-errors (in -Wdefault)]
    • Couldn't match type ‘S r’ with ‘()’
      Expected: ()
        Actual: S r
    • In the first argument of ‘(+)’, namely ‘no’
      In the expression: no + _
      In a case alternative: Refl -> no + _
    • Relevant bindings include
        no :: S r (bound at T15370.hs:18:7)
        right :: S r -> () (bound at T15370.hs:18:1)

T15370.hs:20:18: warning: [-Wtyped-holes (in -Wdefault)]
    • Found hole: _ :: ()
    • In the second argument of ‘(+)’, namely ‘_’
      In the expression: no + _
      In a case alternative: Refl -> no + _
    • Relevant bindings include
        no :: S r (bound at T15370.hs:18:7)
        right :: S r -> () (bound at T15370.hs:18:1)
      Constraints include y ~ x (from T15370.hs:20:5-8)
      Valid hole fits include
        () :: ()
        mempty :: forall a. Monoid a => a
        maxBound :: forall a. Bounded a => a
        minBound :: forall a. Bounded a => a