Getting rid of -XImpredicativeTypes

[Ganesh Sittampalam]

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]
> *Sent:* 26 September 2016 08:13
> *To:* Simon Peyton Jones <simonpj at microsoft.com>
> *Cc:* ghc-users at haskell.org; 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 <mailto: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 <mailto: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 list
> 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/a63ab14a/attachment.html>