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:

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.


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