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
#11319: ImpredicativeTypes even more broken than usual -------------------------------------+------------------------------------- Reporter: Iceland_jack | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.11 checker) | Keywords: Resolution: | ImpredicativeTypes Operating System: Linux | Architecture: | Unknown/Multiple Type of failure: GHC rejects | Test Case: valid program | typecheck/should_compile/T11319 Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by RyanGlScott): Since this ticket was originally opened, SPJ started a [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html very relevant discussion] on the GHC devs mailing list about a way to salvage `ImpredicativeTypes`. It wouldn't make the original program in this ticket typecheck again, but it would provide a way to possibly suggest a workaround in error messages. To quote SPJ: 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.
{{{#!hs 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. However, this should undoubtedly go through a GHC proposal. At the very least, it's unclear to me whether SPJ's intention was to require actually enabling `-XImpredicativeTypes` in order to visibly apply a polytype (the title of the GHC devs discussion, "Getting rid of `-XImpredicativeTypes`", makes me think "no", but the actual contents of the discussion that I quoted would suggest "yes"). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11319#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler