GHC does not support GADTs or type families which witness equality of multiplicities [GHC-59840]

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.

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/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
   | ^^^^^^^^^^^^^^^...

LinearPolyType.hs

Before

{-# 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

After

module LinearPolyType where

-- This program cannot currently be written