``` unison
structural ability X t where
  x : t -> a -> a

structural ability Abort where
  abort : a
```

``` 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 ability Abort
      structural ability X t

```
``` ucm
scratch/main> add

  ⍟ I've added these definitions:
  
    structural ability Abort
    structural ability X t

```
This code should not type check. The match on X.x ought to introduce a
skolem variable `a` such that `c : a` and the continuation has type
`a ->{X} b`. Thus, `handle c with h : Optional a`, which is not the
correct result type.

``` unison
h0 : Request {X t} b -> Optional b
h0 req = match req with
  { X.x _ c -> _ } -> handle c with h0
  { d } -> Some d
```

``` ucm

  Loading changes detected in scratch.u.

  Each case of a match / with expression need to have the same
  type.
  
  Here, one   is:  Optional b
  and another is:  Optional a
  
  
      3 |   { X.x _ c -> _ } -> handle c with h0
  
    from these spots, respectively:
  
      1 | h0 : Request {X t} b -> Optional b
  

```
This code should not check because `t` does not match `b`.

``` unison
h1 : Request {X t} b -> Optional b
h1 req = match req with
  { X.x t _ -> _ } -> handle t with h1
  { d } -> Some d
```

``` ucm

  Loading changes detected in scratch.u.

  Each case of a match / with expression need to have the same
  type.
  
  Here, one   is:  Optional b
  and another is:  Optional t
  
  
      3 |   { X.x t _ -> _ } -> handle t with h1
  
    from these spots, respectively:
  
      1 | h1 : Request {X t} b -> Optional b
  

```
This code should not check for reasons similar to the first example,
but with the continuation rather than a parameter.

``` unison
h2 : Request {Abort} r -> r
h2 req = match req with
  { Abort.abort -> k } -> handle k 5 with h2
  { r } -> r
```

``` ucm

  Loading changes detected in scratch.u.

  The 1st argument to `k`
  
            has type:  Nat
      but I expected:  a
  
      3 |   { Abort.abort -> k } -> handle k 5 with h2
  

```
This should work fine.

``` unison
h3 : Request {X b, Abort} b -> Optional b
h3 = cases
  { r } -> Some r
  { Abort.abort -> _ } -> None
  { X.x b _ -> _ } -> Some b
```

``` 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`:
    
      h3 : Request {X b, Abort} b -> Optional b

```