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@erdi.hu =-------' I love vegetarians - some of my favorite foods are vegetarians.