unison/unison-src/transcripts/fix3196.output.md

Tests ability checking in scenarios where one side is concrete and the other is a variable. This was supposed to be covered, but the method wasn't actually symmetric, so doing equate l r might work, but not equate r l.

Below were cases that caused the failing order.

structural type W es = W

unique ability Zoot where
  zoot : ()

woot : W {g} -> '{g, Zoot} a ->{Zoot} a
woot w a = todo ()

ex = do
  w = (W : W {Zoot})
  woot w do bug "why don't you typecheck?"

w1 : W {Zoot}
w1 = W

w2 : W {g} -> W {g}
w2 = cases W -> W

> w2 w1

  Loading changes detected in scratch.u.

  I found and typechecked these definitions in scratch.u. If you
  do an `add` or `update`, here's how your codebase would
  change:
  
    ⍟ These new definitions are ok to `add`:
    
      structural type W es
      ability Zoot
      ex   : '{Zoot} r
      w1   : W {Zoot}
      w2   : W {g} -> W {g}
      woot : W {g} -> '{g, Zoot} a ->{Zoot} a
  
  Now evaluating any watch expressions (lines starting with
  `>`)... Ctrl+C cancels.

    19 | > w2 w1
           ⧩
           W