#14859: Allow explicit impredicativity -------------------------------------+------------------------------------- Reporter: simonpj | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.2 Keywords: | Operating System: Unknown/Multiple Architecture: | Type of failure: None/Unknown Unknown/Multiple | Test Case: | Blocked By: Blocking: | Related Tickets: Differential Rev(s): | Wiki Page: -------------------------------------+------------------------------------- In [https://mail.haskell.org/pipermail/ghc-devs/2016-September/012940.html this email] I suggested allowing a simple form of impredicativity. With a suitable extension flag (`-XExplicitImpredicativeTypes` perhaps), you woudl be allowed: * To write a polytype in a visible type argument; eg. `f @(forall a. a->a)` * To write a polytype as an argument of a type in a signature e.g. `f :: [forall a. a->a] -> Int` ''But 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 (VTA). 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 at least it's possible. The main motivation is that we are naughtily doing this anyway in the implementation of `GeneralisedNewtypeDeriving` -- see Trac #14070 comment:23 ff. If we are doing it under the hood, we could just made it available to programmers. This is much less ambitious, and much easier to implement, than the proposed [https://www.microsoft.com/en-us/research/publication/guarded- impredicative-polymorphism/ Guarded impredicative polymorphism] (PLDI'18). This ticket just records the idea, to see what other use-cases people might want to add. Then someone would have to write a GHC proposal. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14859 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler