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]) EvBindsVaraCu}
(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 \
`---= ge...@erdi.hu =---'
I love vegetarians - some of my favorite foods are vegetarians.___
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs
