Unifying inferred and declared *existential* type variables
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.
Hi Gergo,
There is indeed something strange about that output. The good news is that I'm not convinced you need `unifyType`, but I'm not sure exactly what you do need.
- There is nothing, in general, inside the `cobox`es. Those are just variables. In the Core you include, they're out of scope, so if that type error weren't reported, Core Lint would complain. Ids with the name "cobox" get created in two places: newEvVar and newEq.
newEvVar is called when GHC needs to quantify over "given" equalities and class predicates. I don't think that's what's happening here though.
newEq is called in the bowels of unifyType, when unifyType fails to unify two types. In this case, the TcCoercion that unifyType produces just wraps the cobox variable, and it is expected that the caller of unifyType will call the constraint simplifier (one of the functions in TcSimplify) with appropriate arguments to figure out what the cobox should be. Then, when desugaring to Core, the cobox is expanded, and we do not have the out-of-scope cobox seen in your output. It seems this call to the simplifier is not happening. (But, I don't think it needs to! Keep reading.)
- Again, looking at the Core, `cont` can be called *without any coercions*. (Well, almost.) Currently, your Core has `cont b $dEq_aCr x y`. The first parameter to `cont` is the type variable. If you pass in `a` (instead of the out-of-scope `b`), `cont`'s type will be instantiated with `a` and the types will then line up. The "Well, almost" is because you pass in an out-of-scope `$dEq_aCr`, where I would expect the in-scope `dEq_aCt` (note the different Unique!). Not sure what's going on here.
- The example code you're trying to process is easy, in that the pattern type signature and the datacon type signature are identical. When this is not the case, I realize further analysis will be required. But, my hunch (which could very well be wrong) is that you want the functions in types/Unify.lhs, not typecheck/TcUnify.lhs. The former walks over types and produces a substitution from one to the other instead of a coercion witnessing equality. Substitution may be all you need here.
I hope this is helpful in spurring on progress!
Richard
On Aug 16, 2014, at 4:29 AM, 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@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
participants (2)
-
Dr. ERDI Gergo -
Richard Eisenberg