Gabriel Dos Reis <g...@integrable-solutions.net>:
> On Wed, Apr 3, 2013 at 8:01 PM, Manuel M T Chakravarty
> <c...@cse.unsw.edu.au> wrote:
>> E.g., given
>> 
>>  type family F a :: *
>> 
>> the equality
>> 
>>  Maybe (forall a. F [a]) ~ G b
>> 
>> would need to be broken down to
>> 
>>  x ~  F [a], Maybe (forall a. x) ~ G b
>> 
>> but you cannot do that, because you just moved 'a' out of its scope. Maybe
>> you can move the forall out as well?
> 
> yes, why wouldn't you pull it out as well:
> 
>   x ~ forall a. F [a], Maybe x ~ G b
> 
> where you systematically introduce fresh  type
> variables for an quantified type expressions?

One universally quantified variable may appear as the argument to two type 
family applications (or more generally, have two occurrences, of which only one 
is under the type family).

Moreover, the whole equality solution mechanism quite fundamentally depends on 
producing equalities of the form

  x ~ F b1 ... bn

for type family applications. Sticking a forall in there may lead to trouble 
with the proof theory. In particular, it would compromise the analogy to CHRs 
(constraint handling rules) which inspired our solution.

Manuel


_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://www.haskell.org/mailman/listinfo/ghc-devs

Reply via email to