Restrictions on polytypes with type families

[Simon Peyton-Jones]

Manuel has an excellent point. See the Note below in TcCanonical!   I have no clue how to deal with this

Simon

Note [Flattening under a forall]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Under a forall, we
  (a) MUST apply the inert subsitution
  (b) MUST NOT flatten type family applications
Hence FMSubstOnly.

For (a) consider   c ~ a, a ~ T (forall b. (b, [c])
If we don't apply the c~a substitution to the second constraint
we won't see the occurs-check error.

For (b) consider  (a ~ forall b. F a b), we don't want to flatten
to     (a ~ forall b.fsk, F a b ~ fsk)
because now the 'b' has escaped its scope.  We'd have to flatten to
       (a ~ forall b. fsk b, forall b. F a b ~ fsk b)
and we have not begun to think about how to make that work!


From: Manuel M T Chakravarty [mailto:chak at cse.unsw.edu.au]
Sent: 04 April 2013 02:01
To: Simon Peyton-Jones
Cc: Iavor Diatchki; ghc-devs
Subject: Re: Restrictions on polytypes with type families

Simon Peyton-Jones <simonpj at microsoft.com<mailto:simonpj at microsoft.com>>:
isn't this moving directly into the territory of impredicative types?

Ahem, maybe you are right.  Impredicativity means that you can
          instantiate a type variable with a polytype

So if we allow, say (Eq (forall a.a->a)) then we've instantiated Eq's type variable with a polytype.  Ditto Maybe (forall a. a->a).

But this is only bad from an inference point of view, especially for implicit instantiation.  Eg if we had
          class C a where
            op :: Int -> a

then if we have
          f :: C (forall a. a->a) =>...
          f = ...op...

do we expect op to be polymorphic??

For type families maybe things are easier because there is no implicit instantiation.

But I'm not sure

These kinds of issues are the reason that my conclusion at the time was (as Richard put it)

Or, are
| there any that are restricted because someone needs to think hard before
| lifting it, and no one has yet done that thinking?

At the time, there were also problems with what the type equality solver was supposed to do with foralls.


I know, for example,
| that the unify function in types/Unify.lhs will have to be completed to
| work with foralls, but this doesn't seem hard.

The solver changed quite a bit since I rewrote Tom's original prototype. So, maybe it is easy now, but maybe it is more tricky than you think. The idea of rewriting complex terms into equalities at the point of each application of a type synonym family (aka type function) assumes that you can pull subterms out of a term into a separate equality, but how is this going to work if a forall is in the way?  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?

Manuel



-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130405/35f58eb2/attachment.htm>