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@gmail.com]
Sent: 26 September 2016 08:13
To: Simon Peyton Jones <simonpj@microsoft.com>
Cc: ghc-users@haskell.org; ghc-devs@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@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@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

 

_______________________________________________
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs