Getting rid of -XImpredicativeTypes

[Carter Schonwald]

On a more inane front,  does this give a path to either making $ less
magical, or better user facing errors when folks use compose (.) style code
instead and hit impredicativtity issues that $ magic would have handled ?

On Sunday, October 2, 2016, Ganesh Sittampalam <ganesh at earth.li> wrote:

> Elsewhere in the thread, you said
>
> 1) ImpredicativeTypes enables types like `Maybe (forall a. a)`. Do those
> just disappear, or are they also enabled anyway? (I would guess the former.)
> Yes, they’d disappear.
>
>
> but here you're talking about 'xs :: [forall a . a->a]' being possible
> with VTA - is the idea that such types will be possible but only with both
> explicit signatures and VTA?
>
> On 30/09/2016 16:29, Simon Peyton Jones via ghc-devs wrote:
>
> Alejandro: excellent point. I mis-spoke before.  In my proposal we WILL
> allow types like (Tree (forall a. a->a)).
>
>
>
> I’m trying to get round to writing a proposal (would someone else like to
> write it – it should be short), but the idea is this:
>
>
>
> *When you have -XImpredicativeTypes*
>
> ·         *You can write a polytype in a visible type argument; eg.  f
> @(forall a. a->a)*
>
> ·         *You can write a polytype as an argument of a type in a
> signature  e.g.  f :: [forall a. a->a] -> Int*
>
>
>
> *And that’s all.  A unification variable STILL CANNOT be unified with a
> polytype.  The only way you can call a polymorphic function at a polytype
> is to use Visible Type Application.*
>
>
>
> *So using impredicative types might be tiresome.  E.g.*
>
> *  type SID = forall a. a->a*
>
>
>
> *  xs :: [forall a. a->a]*
>
> *  xs = (:) @SID id ( (:) @SID id ([] @ SID))*
>
>
>
> *In short, if you call a function at a polytype, you must use VTA.
> Simple, easy, predictable; and doubtless annoying.  But possible*.
>
>
>
> Simon
>
>
>
> *From:* Alejandro Serrano Mena [mailto:trupill at gmail.com
> <javascript:_e(%7B%7D,'cvml','trupill at gmail.com');>]
> *Sent:* 26 September 2016 08:13
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> <javascript:_e(%7B%7D,'cvml','simonpj at microsoft.com');>
> *Cc:* ghc-users at haskell.org
> <javascript:_e(%7B%7D,'cvml','ghc-users at haskell.org');>;
> ghc-devs at haskell.org
> <javascript:_e(%7B%7D,'cvml','ghc-devs at haskell.org');>
> *Subject:* Re: Getting rid of -XImpredicativeTypes
>
>
>
> What would be the story for the types of the arguments. Would I be allowed
> to write the following?
>
> > f (lst :: [forall a. a -> a]) = head @(forall a. a -> a) lst 3
>
> Regards,
>
> Alejandro
>
>
>
> 2016-09-25 20:05 GMT+02:00 Simon Peyton Jones via ghc-devs <
> ghc-devs at haskell.org
> <javascript:_e(%7B%7D,'cvml','ghc-devs at haskell.org');>>:
>
> Friends
>
>
>
> GHC has a flag -XImpredicativeTypes that makes a half-hearted attempt to
> support impredicative polymorphism.  But it is vestigial…. if it works,
> it’s really a fluke.  We don’t really have a systematic story here at all.
>
>
>
> I propose, therefore, to remove it entirely.  That is, if you use
> -XImpredicativeTypes, you’ll get a warning that it does nothing (ie.
> complete no-op) and you should remove it.
>
>
>
> Before I pull the trigger, does anyone think they are using it in a
> mission-critical way?
>
>
>
> Now that we have Visible Type Application there is a workaround: if you
> want to call a polymorphic function at a polymorphic type, you can
> explicitly apply it to that type.  For example:
>
>
>
> {-# LANGUAGE ImpredicativeTypes, TypeApplications, RankNTypes #-}
>
> module Vta where
>
>   f x = id @(forall a. a->a) id @Int x
>
>
>
> You can also leave out the @Int part of course.
>
>
>
> Currently we have to use -XImpredicativeTypes to allow the @(forall a.
> a->a).    Is that sensible?  Or should we allow it regardless?   I rather
> think the latter… if you have Visible Type Application (i.e.
> -XTypeApplications) then applying to a polytype is nothing special.   So I
> propose to lift that restriction.
>
>
>
> I should go through the GHC Proposals Process for this, but I’m on a
> plane, so I’m going to at least start with an email.
>
>
>
> Simon
>
>
> _______________________________________________
> ghc-devs mailing list
> ghc-devs at haskell.org
> <javascript:_e(%7B%7D,'cvml','ghc-devs at haskell.org');>
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
> <https://na01.safelinks.protection.outlook.com/?url=http%3A%2F%2Fmail.haskell.org%2Fcgi-bin%2Fmailman%2Flistinfo%2Fghc-devs&data=01%7C01%7Csimonpj%40microsoft.com%7Cd4eb1fd61d0148cea9f508d3e5dca6fe%7C72f988bf86f141af91ab2d7cd011db47%7C1&sdata=ZM3djztmpA09J6x1DmmV0LEeftsA1FhjPhjwLuG5w%2FE%3D&reserved=0>
>
>
>
>
> _______________________________________________
> ghc-devs mailing listghc-devs at haskell.org <javascript:_e(%7B%7D,'cvml','ghc-devs at haskell.org');>http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
>
>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/ghc-devs/attachments/20161002/15118839/attachment.html>