[darcs-users] [patch40] stop using impredicativity

[Ganesh Sittampalam]

On Wed, 30 Jun 2010, Eric Kow wrote:

> On Sat, Jun 26, 2010 at 16:35:22 +0000, Ganesh Sittampalam wrote:

>>  type CommuteFunction = FORALL(x y) (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y))
>> -subcommutes :: [(String, CommuteFunction)]
>> +subcommutes :: [(String, (Prim :< Prim) C(x y) -> Perhaps ((Prim :< Prim) C(x y)))]
>
> I'm not clear on why this particular change is necessary and suspect it
> just slipped in by accident

No, it is necessary :-) CommuteFunction has an explicit forall - it's just 
a type alias and those get expanded at each use site, so the old code had 
a forall inside the tuple type.

Imagine that pairs are explicitly defined as a Haskell datatype rather 
than being part of the language. The definition might look something like 
this:

data (a, b) = (a, b)

In other words a pair is something that takes two type variables as type 
parameters. As you say in the rest of your review, impredicativity makes 
it legal to instantiate those variables with types that have a top-level 
forall. Without impredicativity, that isn't legal so we have to change it 
somehow. It turns out that in this case the forall there isn't actually 
needed so I just remove it.

> This is the main change
>
>>  restrictSubpaths :: (RepoPatch p) => Repository p C(r u t) -> [SubPath]
>> -                 -> IO (forall t m. FilterTree t m => t m -> t m)
>> +                 -> IO (TreeFilter m)
>
> and a particular example of the change in action.
>
> I'm guessing here we actually never needed that inner forall m in the
> first place and were only using impredicativity for t.

Correct. (I guessed that too and the type checker confirmed it for me :-)

Ganesh