Unifying inferred and declared *existential* type variables

[Dr. ERDI Gergo]

Hi,

Background:

Type signatures for pattern synonyms are / can be explicit about the 
existentially-bound type variables of the pattern. For example, given the 
following definitions:

data T where
   C :: (Eq a) => [a] -> (a, Bool) -> T

pattern P x y = C x y

the inferred type of P (with explicit foralls printed) is

pattern type forall a. Eq a => P [a] (a, Bool) :: T


My problem:

Ticket #8968 is a good example of a situation where we need this 
pattern type signature to be entered by the user. So continuing with the 
previous example, the user should be able to write, e.g.

pattern type forall b. Eq b => P [b] (b, Bool) : T

So in this case, I have to unify the argument types [b] ~ [a] and (b, 
Bool) ~ (a, Bool), and then use the resulting coercions of the 
existentially-bound variables before calling the success continuation.

So I generate a pattern synonym matcher as such (going with the previous 
example) (I've pushed my code to wip/T8584):

  $mP{v r0} :: forall t [sk].
       T
       -> (forall b [sk]. Eq b [sk] => [b [sk]] -> (b [sk], Bool) -> t [sk])
       -> t [sk]
       -> t [sk]
  $mP{v r0}
    = /\(@ t [sk]).
      \ ((scrut [lid] :: T))
        ((cont [lid] :: forall b [sk]. Eq b [sk] => [b [sk]] -> (b [sk], Bool) -> t [sk]))
        ((fail [lid] :: t [sk]))
        -> case scrut
           of {
             C {@ a [ssk] ($dEq_aCt [lid] :: Eq a [ssk]) EvBindsVar<aCu>}
               (x [lid] :: [a [ssk]])
               (y [lid] :: (a [ssk], Bool))
               -> cont b $dEq_aCr x y
                    |> (cobox{v} [lid], <Bool>_N)_N
                    |> [cobox{v} [lid]]_N }
  <>}

The two 'cobox'es are the results of unifyType'ing [a] with [b] and (a, 
Bool) with (b, Bool). So basically what I hoped to do was to pattern-match 
on 'C{@ a $dEqA} x y' and pass that to cont as 'b' and '$dEqB' by 
rewriting them  with the coercions. (It's unfortunate that even with full 
-dppr-debug output, I can't see what's inside the 'cobox'es).

However, when I try doing this, I end up with the error message

SigGADT2.hs:10:9:
     Couldn't match type ‘a [ssk]’ with ‘b [sk]’
       because type variable ‘b [sk]’ would escape its scope
     This (rigid, skolem) type variable is bound by
       the type signature for
         P :: [b [sk]] -> (b [sk], Bool) -> T
       at SigGADT2.hs:10:9
     Expected type: [b [sk]]
       Actual type: [a [ssk]]

Also, while the result of unifying '[b]' ~ '[a]' and '(b, Bool)' ~
'(a, Bool)' should take care of turning the 'a' bound by the constructor 
into the 'b' expected by the continuation function, it seems to me I'll 
need to do some extra magic to also turn the bound 'Eq a' evidence 
variable into the 'Eq b'.

Obviously, I am missing a ton of stuff here. Can someone help me out?

Thanks,
 	Gergo

-- 

   .--= ULLA! =-----------------.
    \     http://gergo.erdi.hu   \
     `---= gergo at erdi.hu =-------'
I love vegetarians - some of my favorite foods are vegetarians.