Document GHC-59840 (#450)

* Document GHC-59840

* Apply suggestions from code review

Co-authored-by: David Thrane Christiansen <[email protected]>

* Apply suggestion from code review

---------

Co-authored-by: David Thrane Christiansen <[email protected]>

Author: BinderDavid

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

@@ -0,0 +1,16 @@
+---
+title: GHC does not support GADTs or type families which witness equality of multiplicities
+summary: GHC does not support GADTs or type families which witness equality of multiplicities
+severity: error
+introduced: 9.6.1
+---
+
+There are two features which GHC supports, and whose interaction is problematic and leads to this error:
+
+- Programming constructs which build upon the type equality constraint `a ~ b`, such as GADTs and type families.
+- Linear types, which supports functions like `a %m -> b`. In this function type `m` stands for a *multiplicity* which can be either `One`(also written `1`) or `Many`, which determines how often the argument to the function may be used in the body of the function.
+
+Problems arise when the type equality constraint `a ~ b` is used for multiplicities, i.e. when we encounter equalities like `m1 ~ m2`.
+Until the interaction between equality constraints and multiplicities is better understood, GHC decides to not support equalities between multiplicities, or features which require them.
+
+More information about this particular interaction can be found on the [GHC issue tracker](https://gitlab.haskell.org/ghc/ghc/-/issues/19517).

message-index/messages/GHC-59840/linearPolyType/after/LinearPolyType.hs

@@ -0,0 +1,3 @@
+module LinearPolyType where
+
+-- This program cannot currently be written

message-index/messages/GHC-59840/linearPolyType/before/LinearPolyType.hs

@@ -0,0 +1,15 @@
+{-# LANGUAGE LinearTypes, GADTs, KindSignatures, DataKinds, TypeFamilies, PolyKinds #-}
+module LinearPolyType where
+
+import GHC.Types
+data SBool :: Bool -> Type where
+  STrue :: SBool True
+  SFalse :: SBool False
+
+type family If b t f where
+  If True t _ = t
+  If False _ f = f
+
+dep :: SBool b -> Int %(If b One Many) -> Int
+dep STrue x = x
+dep SFalse _ = 0

message-index/messages/GHC-59840/linearPolyType/index.md

@@ -0,0 +1,14 @@
+---
+title: Computing a multiplicity with a type family and GADT is not supported
+---
+
+This example of an interaction between multiplicities and type equalities was discussed in the[GHC proposal](https://github.com/ghc-proposals/ghc-proposals/pull/111#issuecomment-438125526) which introduced linear types.
+There is no theoretical problem with this program, but the type inference mechanisms that GHC currently uses cannot typecheck it.
+
+```
+messages/GHC-59840/linearPolyType/before/LinearPolyType.hs:14:1: error: [GHC-59840]
+    GHC bug #19517: GHC currently does not support programs using GADTs or type families to witness equality of multiplicities
+   |
+14 | dep STrue x = x
+   | ^^^^^^^^^^^^^^^...
+```