Inconsistency in flexibility of patterns and nested patterns

[mpickering]

In an email with Craig, he pointed out a workaround to a problem I had been having.
Playing around with his workaround highlighted an inconsistency with how patterns are type checked.

In handleModifyPlayOrder, I can pattern match on MkEC and then use the effect polymorphic computation in an environment which has access to the State ability.

If I try to write a top level definition, not a handler, h, which does the same thing but does not handle an effect then the use of f is rejected.

on : X -> {X -> Y} -> Y
on x g = g x

interface ModifyOrder [E] = modifyOrder : EndoComp (List X) -> Unit

data EndoComp Y = MkEC {Y -> Y}

---
rotate : List X -> List X
rotate x = x

data S = S (List P)

interface State = get : S | put : S -> Unit

handleModifyPlayOrder : <ModifyOrder>X -> [State]X
handleModifyPlayOrder x = x
handleModifyPlayOrder <modifyOrder (MkEC f) -> k> =
  on get! { (S po) -> put (S (f po)); handleModifyPlayOrder (k unit) }

-- This doesn't type check
--h : EndoComp (List X) -> [State]Unit
--h (MkEC f) =
--  on get! { (S po) -> put (S (f po)) }

main : { [Console]Unit }
main! = unit

= Analysis

There seems to be an inconsistency about where makeFlexible is called.

In the first definition, the type checking first enters checkPat and then the case for MkCmdPat. Then crucially,
in the Just branch, makeFlexible is mapped over the types of the patterns. checkVPat is then called on each of the patterns with these flexible types.

In the second case, checkPat is called directly from checkCls which doesn't call makeFlexible on the result type which means the rigid type variable (X$r10) causes unification to fail.

This means that the arguments to checkVPat look like this, notice the subtle difference of MkRVar vs MkFVar.

For the handler:
Pattern Type: MkDTTy "EndoComp" [VArg (MkDTTy "List" [VArg (MkFTVar "X$f1")])
Args Type: EArg (MkAb (MkAbFVar "\163$f2") (fromList []))],[VArg (MkFTVar "Y$f3"),EArg (MkAb (MkAbFVar "\163$f4") (fromList []))])

For h:
Pattern Type: MkDTTy "EndoComp" [VArg (MkDTTy "List" [VArg (MkRTVar "X$r10")])
Args Type: EArg (MkAb (MkAbRVar "\163$r7") (fromList []))],[VArg (MkFTVar "Y$f0"),EArg (MkAb (MkAbFVar "\163$f1") (fromList []))])