Document GHC-91028 (#454)

* Document GHC-91028

Fixes #24
Fixes #453

* Replace undefined with Proxy in GHC-91028 per suggestion

message-index/messages/GHC-91028/impred/after/Impred.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+module Impred where
+
+import Control.Monad.ST
+
+test :: (forall s. ST s a) -> a
+test = id runST

message-index/messages/GHC-91028/impred/before/Impred.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE RankNTypes #-}
+module Impred where
+
+import Control.Monad.ST
+
+test :: (forall s. ST s a) -> a
+test = id runST

message-index/messages/GHC-91028/impred/index.md

@@ -0,0 +1,39 @@
+---
+title: Enabling Impredicativity
+---
+
+## Error
+```
+Impred.hs:7:8: error: [GHC-91028]
+    • Couldn't match expected type ‘(forall s. ST s a) -> a’
+                  with actual type ‘a0’
+      Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: (forall s. ST s a) -> a
+    • In the expression: id runST
+      In an equation for ‘test’: test = id runST
+    • Relevant bindings include
+        test :: (forall s. ST s a) -> a (bound at Impred.hs:7:1)
+  |
+7 | test = id runST
+  |        ^^^^^^^^
+
+Impred.hs:7:11: error: [GHC-91028]
+    • Couldn't match expected type ‘a0’
+                  with actual type ‘(forall s. ST s a1) -> a1’
+      Cannot instantiate unification variable ‘a0’
+      with a type involving polytypes: (forall s. ST s a1) -> a1
+    • In the first argument of ‘id’, namely ‘runST’
+      In the expression: id runST
+      In an equation for ‘test’: test = id runST
+  |
+7 | test = id runST
+  |           ^^^^^
+```
+
+## Explanation
+
+Some code truly needs impredicativity. In this example, `runST` has the type `(forall s. ST s a) -> a`. Because the `forall` is nested underneath the arrow, GHC can't just provide it with a type argument - indeed, `runST` is one of the motivating examples for the utility of higher-rank polymorphism, and impredicativity removes restrictions from the uses of higher-rank functions. But applying `id` to `runST` requires instantiating the type variable in `id` to `(forall s. ST s a) -> a`, which is polymorphic.
+
+Here, the error occurs twice: once when GHC attempts to match the type of `id`'s argument to the type of `runST`, and again when it attempts to match `id`'s return type to the type signature on `test`. In each case, the type variable `a0` from `id`'s type `forall a0. a0 -> a0` is needed.
+
+This code can be fixed by turning on impredicative polymorphism, which implies `RankNTypes`.

message-index/messages/GHC-91028/index.md

@@ -0,0 +1,22 @@
+---
+title: Cannot equate polymorphic types with type variables
+summary: During type inference, GHC can't instantiate a type variable with a type that is itself polymorphic.
+severity: error
+introduced: 9.6.1
+---
+
+During the type checking process, type variables are replaced with actual types. For example, the function `id` has type `a -> a`, which is a shorter way of writing `forall a. a -> a`. When `id` is applied to an argument, the variable `a` is _instantiated_ with the argument's type, causing `id`'s return type (and thus the whole expression) to be the same as the argument's type. This is because `id`'s type is _polymorphic_ - it contains variables that can be instantiated with many different types.
+
+For technical reasons, type variables cannot be instantiated with types that are themselves polymorphic in Haskell. This kind of instantiation is referred to as [_impredicative_](https://en.wikipedia.org/wiki/Impredicativity), borrowing a term from logic that describes terms with quantifiers where the variable ranges over the same set as the one in which the quantifier is being used. Haskell is _predicative_, meaning that the variables of the `forall` quantifier do not range over types that themselves contain `forall`. Predicativity makes a type system much less expressive, which means that implementations are able to be more predictable for users, run faster, and give better error messages. Impredicativity is sometimes very useful, but predicativity is usually strong enough.
+
+This error occurs when GHC is asked to instantiate a type variable with a polymorphic type, which would require impredicativity.
+
+## Enabling Impredicativity
+
+For some time, GHC has supported an extension called `ImpredicativeTypes`, but it was unreliable for many years. Starting in version 9.2, GHC uses a new implementation of type inference with impredicativity called [Quick Look](https://www.microsoft.com/en-us/research/publication/a-quick-look-at-impredicativity/) that is more robust than previous implementations, so `ImpredicativeTypes` is now considered suitable for serious use. If your application does require the additional power provided by impredicativity, then enabling this extension may resolve this error message. Code that uses `ImpredicativeTypes` is likely to be less compatible with GHC 9.0 and earlier due to the revamping of this extension.
+
+## Impredicative Kinds
+
+Types and kinds are unified into a single entity in GHC, with typing rules rather than a separate grammar being used to track the difference between them. GHC's kind system thus supports many features of the type system, including polymorphism. A definition may be polymorphic over both types and kinds. This error can also occur when GHC attempts to instantiate a kind variable with a polymorphic kind.
+
+However, even when `ImpredicativeTypes` is enabled, GHC requires that kind polymorphism be predicative.

message-index/messages/GHC-91028/predkinds/after/PredKinds.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+module PredKinds where
+
+import Data.Proxy
+
+t :: forall a (z :: forall k. a). Proxy z
+t = Proxy

message-index/messages/GHC-91028/predkinds/before/PredKinds.hs

@@ -0,0 +1,7 @@
+{-# LANGUAGE ImpredicativeTypes #-}
+module PredKinds where
+
+import Data.Proxy
+
+t :: Proxy (z :: forall k. a)
+t = Proxy

message-index/messages/GHC-91028/predkinds/index.md

@@ -0,0 +1,32 @@
+---
+title: Impredicative Kind Polymorphism
+---
+
+## Error
+```
+PredKinds.hs:6:13: error: [GHC-91028]
+    • Expected kind ‘forall (k :: k1). a’, but ‘z’ has kind ‘k0’
+      Cannot instantiate unification variable ‘k0’
+      with a kind involving polytypes: forall (k2 :: k1). a
+    • In the first argument of ‘Proxy’, namely ‘(z :: forall k. a)’
+      In the type signature: t :: Proxy (z :: forall k. a)
+  |
+6 | t :: Proxy (z :: forall k. a)
+  |             ^
+```
+
+## Explanation
+
+Even when impredicative types are enabled, polymorphic kinds remain predicative. In this case, the type constructor `Proxy` has the kind `forall k. k -> Type`. This allows its argument to be any type, no matter its kind. Applying it to the type `(z :: forall k. a)` would require instantiating `Proxy`'s kind argument `k` with the polymorphic kind `forall k. a`, but this is not allowed.
+
+The only way to fix this error is to rewrite the code so that impredicative polymorphism is not required. One way to do this is to lift the polymorphism outward, so that GHC will suitably instantiate the type `z`'s polymorphic arguments in the argument position to `Proxy`. After performing this transformation, the fully explicit type of `t` can be seen in GHCI:
+```
+ghci> :l PredKinds.hs
+[1 of 1] Compiling PredKinds        ( PredKinds.hs, interpreted )
+Ok, one module loaded.
+ghci> :set -fprint-explicit-kinds
+ghci> :t t
+t :: forall {k1} {k2 :: k1} a (z :: forall (k3 :: k1). a).
+     Proxy @{a} (z @k2)
+```
+Here, GHC has provided the argument `k2` to `z`, resulting in a type with a monomorphic kind `a`.