Restrictions on polytypes with type families

[Gábor Lehel]

On Fri, Apr 5, 2013 at 1:32 PM, Dimitrios Vytiniotis <dimitris at microsoft.com
> wrote:

>  Hmm, no I don’t think that Flattening is a very serious problem:
>
> Firstly, we can somehow get around that if we use implication constraints
> and higher-order flattening
>
> variables. We have discussed that (but not implemented). For example.
>
>
>
> forall a. F [a] ~ G Int
>
>
>
> becomes:
>
>
>
> forall a.  fsk a ~ G Int
>
>
>
> forall a. true => fsk a ~ F [a]
>
>
>
> Secondly:  flattening under a Forall is not terribly important, unless you
> have type families that dispatch on
>
> polymorphic types, which is admittedly a rather rare case. We lose some
> completeness but that’s ok.
>
>
>
> For me, a more serious problem are polymorphic RHS, which give rise to
> exactly the same problems for type
>
> inference as impredicative polymorphism. For instance:
>
>
>
> type instance F Int = forall a. a -> [a]
>
>
>
> g :: F Int
>
> g = undefined
>
>
>
> main = g 3
>
>
>
> Should this type check or not? And then all our discussions about
> impredicativity, explicit type applications etc become
>
> relevant again.
>
>
>
> Thanks!
>
> d-
>

If the problem with foralls on the RHS is that it devolves into
ImpredicativeTypes, what about only allowing them when ImpredicativeTypes
is on?


>
>
>
>
>
>
>
>
>
> *From:* Simon Peyton-Jones
> *Sent:* Friday, April 05, 2013 8:24 AM
> *To:* Manuel M T Chakravarty
> *Cc:* Iavor Diatchki; ghc-devs; Dimitrios Vytiniotis
> *Subject:* RE: Restrictions on polytypes with type families
>
>
>
> 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<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>:
>
>  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
>
>
>
>
>
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> http://www.haskell.org/mailman/listinfo/ghc-devs
>
>


-- 
Your ship was destroyed in a monadic eruption.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://www.haskell.org/pipermail/ghc-devs/attachments/20130405/769c8aa5/attachment-0001.htm>