FW: Getting rid of -XImpredicativeTypes

[Simon Peyton Jones]

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
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20160926/9afb6d9f/attachment.html>
-------------- next part --------------
An embedded and charset-unspecified text was scrubbed...
Name: ATT00001.txt
URL: <http://mail.haskell.org/pipermail/glasgow-haskell-users/attachments/20160926/9afb6d9f/attachment.txt>