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.

``` unison
structural type W es = W

unique ability Zoot where
  zoot : ()

-- here only to put a kind constraint on W
structural type C = C (W {})

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
```

``` ucm

  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 C
      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.

    22 | > w2 w1
           ⧩
           W

```