GHC does not support GADTs or type families which witness equality of multiplicities [GHC59840]
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 typem
stands for a multiplicity which can be eitherOne
(also written1
) orMany
, 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.
Examples
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 theGHC proposal 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/GHC59840/linearPolyType/before/LinearPolyType.hs:14:1: error: [GHC59840]
GHC bug #19517: GHC currently does not support programs using GADTs or type families to witness equality of multiplicities

14  dep STrue x = x
 ^^^^^^^^^^^^^^^...
LinearPolyType.hs
{# 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
module LinearPolyType where
 This program cannot currently be written