.gitlab-ci.yml

@@ -287,6 +287,9 @@ lint-submods:
   rules:
     - if: '$CI_MERGE_REQUEST_LABELS =~ /.*marge_bot_batch_merge_job.*/'
       allow_failure: false
+    # Don't run on nightly because the program needs a base commit to check.
+    - if: $NIGHTLY
+      when: never
     - allow_failure: true
 
 lint-submods-branch:

compiler/GHC.hs

@@ -197,7 +197,7 @@ module GHC (
         TyCon,
         tyConTyVars, tyConDataCons, tyConArity,
         isClassTyCon, isTypeSynonymTyCon, isTypeFamilyTyCon, isNewTyCon,
-        isPrimTyCon, isFunTyCon,
+        isPrimTyCon,
         isFamilyTyCon, isOpenFamilyTyCon, isOpenTypeFamilyTyCon,
         tyConClass_maybe,
         synTyConRhs_maybe, synTyConDefn_maybe, tyConKind,

compiler/GHC/Builtin/Names.hs

@@ -258,6 +258,7 @@ basicKnownKeyNames
         starKindRepName,
         starArrStarKindRepName,
         starArrStarArrStarKindRepName,
+        constraintKindRepName,
 
         -- WithDict
         withDictClassName,
@@ -333,6 +334,9 @@ basicKnownKeyNames
         fromListNName,
         toListName,
 
+        -- Non-empty lists
+        nonEmptyTyConName,
+
         -- Overloaded record dot, record update
         getFieldName, setFieldName,
 
@@ -1401,14 +1405,19 @@ typeCharTypeRepName   = varQual tYPEABLE_INTERNAL (fsLit "typeCharTypeRep") type
 trGhcPrimModuleName   = varQual gHC_TYPES         (fsLit "tr$ModuleGHCPrim")  trGhcPrimModuleKey
 
 -- Typeable KindReps for some common cases
-starKindRepName, starArrStarKindRepName, starArrStarArrStarKindRepName :: Name
-starKindRepName        = varQual gHC_TYPES         (fsLit "krep$*")         starKindRepKey
-starArrStarKindRepName = varQual gHC_TYPES         (fsLit "krep$*Arr*")     starArrStarKindRepKey
-starArrStarArrStarKindRepName = varQual gHC_TYPES  (fsLit "krep$*->*->*")   starArrStarArrStarKindRepKey
+starKindRepName, starArrStarKindRepName,
+  starArrStarArrStarKindRepName, constraintKindRepName :: Name
+starKindRepName        = varQual gHC_TYPES         (fsLit "krep$*")          starKindRepKey
+starArrStarKindRepName = varQual gHC_TYPES         (fsLit "krep$*Arr*")      starArrStarKindRepKey
+starArrStarArrStarKindRepName = varQual gHC_TYPES  (fsLit "krep$*->*->*")    starArrStarArrStarKindRepKey
+constraintKindRepName  = varQual gHC_TYPES         (fsLit "krep$Constraint") constraintKindRepKey
 
 -- WithDict
 withDictClassName :: Name
-withDictClassName     = clsQual gHC_MAGIC_DICT (fsLit "WithDict") withDictClassKey
+withDictClassName = clsQual gHC_MAGIC_DICT (fsLit "WithDict") withDictClassKey
+
+nonEmptyTyConName :: Name
+nonEmptyTyConName = tcQual gHC_BASE (fsLit "NonEmpty") nonEmptyTyConKey
 
 -- Custom type errors
 errorMessageTypeErrorFamName
@@ -1783,7 +1792,7 @@ hasFieldClassNameKey = mkPreludeClassUnique 50
 
 addrPrimTyConKey, arrayPrimTyConKey, boolTyConKey,
     byteArrayPrimTyConKey, charPrimTyConKey, charTyConKey, doublePrimTyConKey,
-    doubleTyConKey, floatPrimTyConKey, floatTyConKey, funTyConKey,
+    doubleTyConKey, floatPrimTyConKey, floatTyConKey, fUNTyConKey,
     intPrimTyConKey, intTyConKey, int8TyConKey, int16TyConKey,
     int8PrimTyConKey, int16PrimTyConKey, int32PrimTyConKey, int32TyConKey,
     int64PrimTyConKey, int64TyConKey,
@@ -1794,7 +1803,8 @@ addrPrimTyConKey, arrayPrimTyConKey, boolTyConKey,
     ratioTyConKey, rationalTyConKey, realWorldTyConKey, stablePtrPrimTyConKey,
     stablePtrTyConKey, eqTyConKey, heqTyConKey, ioPortPrimTyConKey,
     smallArrayPrimTyConKey, smallMutableArrayPrimTyConKey,
-    stringTyConKey :: Unique
+    stringTyConKey,
+    ccArrowTyConKey, ctArrowTyConKey, tcArrowTyConKey :: Unique
 addrPrimTyConKey                        = mkPreludeTyConUnique  1
 arrayPrimTyConKey                       = mkPreludeTyConUnique  3
 boolTyConKey                            = mkPreludeTyConUnique  4
@@ -1806,7 +1816,7 @@ doublePrimTyConKey                      = mkPreludeTyConUnique  9
 doubleTyConKey                          = mkPreludeTyConUnique 10
 floatPrimTyConKey                       = mkPreludeTyConUnique 11
 floatTyConKey                           = mkPreludeTyConUnique 12
-funTyConKey                             = mkPreludeTyConUnique 13
+fUNTyConKey                             = mkPreludeTyConUnique 13
 intPrimTyConKey                         = mkPreludeTyConUnique 14
 intTyConKey                             = mkPreludeTyConUnique 15
 int8PrimTyConKey                        = mkPreludeTyConUnique 16
@@ -1837,6 +1847,10 @@ stablePtrTyConKey                       = mkPreludeTyConUnique 39
 eqTyConKey                              = mkPreludeTyConUnique 40
 heqTyConKey                             = mkPreludeTyConUnique 41
 
+ctArrowTyConKey                       = mkPreludeTyConUnique 42
+ccArrowTyConKey                       = mkPreludeTyConUnique 43
+tcArrowTyConKey                       = mkPreludeTyConUnique 44
+
 statePrimTyConKey, stableNamePrimTyConKey, stableNameTyConKey,
     mutVarPrimTyConKey, ioTyConKey,
     wordPrimTyConKey, wordTyConKey, word8PrimTyConKey, word8TyConKey,
@@ -1887,16 +1901,21 @@ voidTyConKey                            = mkPreludeTyConUnique 85
 nonEmptyTyConKey :: Unique
 nonEmptyTyConKey                        = mkPreludeTyConUnique 86
 
+dictTyConKey :: Unique
+dictTyConKey                            = mkPreludeTyConUnique 87
+
 -- Kind constructors
 liftedTypeKindTyConKey, unliftedTypeKindTyConKey,
-  tYPETyConKey, liftedRepTyConKey, unliftedRepTyConKey,
+  tYPETyConKey, cONSTRAINTTyConKey,
+  liftedRepTyConKey, unliftedRepTyConKey,
   constraintKindTyConKey, levityTyConKey, runtimeRepTyConKey,
   vecCountTyConKey, vecElemTyConKey,
   zeroBitRepTyConKey, zeroBitTypeTyConKey :: Unique
 liftedTypeKindTyConKey                  = mkPreludeTyConUnique 88
 unliftedTypeKindTyConKey                = mkPreludeTyConUnique 89
-tYPETyConKey                            = mkPreludeTyConUnique 90
-constraintKindTyConKey                  = mkPreludeTyConUnique 92
+tYPETyConKey                            = mkPreludeTyConUnique 91
+cONSTRAINTTyConKey                      = mkPreludeTyConUnique 92
+constraintKindTyConKey                  = mkPreludeTyConUnique 93
 levityTyConKey                          = mkPreludeTyConUnique 94
 runtimeRepTyConKey                      = mkPreludeTyConUnique 95
 vecCountTyConKey                        = mkPreludeTyConUnique 96
@@ -1918,7 +1937,6 @@ trNameTyConKey                          = mkPreludeTyConUnique 106
 kindRepTyConKey                         = mkPreludeTyConUnique 107
 typeLitSortTyConKey                     = mkPreludeTyConUnique 108
 
-
 -- Generics (Unique keys)
 v1TyConKey, u1TyConKey, par1TyConKey, rec1TyConKey,
   k1TyConKey, m1TyConKey, sumTyConKey, prodTyConKey,
@@ -2067,8 +2085,7 @@ charDataConKey, consDataConKey, doubleDataConKey, falseDataConKey,
     floatDataConKey, intDataConKey, nilDataConKey,
     ratioDataConKey, stableNameDataConKey, trueDataConKey, wordDataConKey,
     word8DataConKey, ioDataConKey, heqDataConKey,
-    coercibleDataConKey, eqDataConKey, nothingDataConKey, justDataConKey,
-    nonEmptyDataConKey :: Unique
+    eqDataConKey, nothingDataConKey, justDataConKey :: Unique
 
 charDataConKey                          = mkPreludeDataConUnique  1
 consDataConKey                          = mkPreludeDataConUnique  2
@@ -2087,7 +2104,6 @@ trueDataConKey                          = mkPreludeDataConUnique 14
 wordDataConKey                          = mkPreludeDataConUnique 15
 ioDataConKey                            = mkPreludeDataConUnique 16
 heqDataConKey                           = mkPreludeDataConUnique 18
-nonEmptyDataConKey                      = mkPreludeDataConUnique 19
 
 -- Generic data constructors
 crossDataConKey, inlDataConKey, inrDataConKey, genUnitDataConKey :: Unique
@@ -2105,7 +2121,10 @@ ordLTDataConKey                         = mkPreludeDataConUnique 27
 ordEQDataConKey                         = mkPreludeDataConUnique 28
 ordGTDataConKey                         = mkPreludeDataConUnique 29
 
+mkDictDataConKey :: Unique
+mkDictDataConKey                        = mkPreludeDataConUnique 30
 
+coercibleDataConKey :: Unique
 coercibleDataConKey                     = mkPreludeDataConUnique 32
 
 staticPtrDataConKey :: Unique
@@ -2249,7 +2268,7 @@ naturalNBDataConKey       = mkPreludeDataConUnique 124
 ************************************************************************
 -}
 
-wildCardKey, absentErrorIdKey, augmentIdKey, appendIdKey,
+wildCardKey, absentErrorIdKey, absentConstraintErrorIdKey, augmentIdKey, appendIdKey,
     buildIdKey, foldrIdKey, recSelErrorIdKey,
     seqIdKey, eqStringIdKey,
     noMethodBindingErrorIdKey, nonExhaustiveGuardsErrorIdKey,
@@ -2266,6 +2285,7 @@ absentErrorIdKey              = mkPreludeMiscIdUnique  1
 augmentIdKey                  = mkPreludeMiscIdUnique  2
 appendIdKey                   = mkPreludeMiscIdUnique  3
 buildIdKey                    = mkPreludeMiscIdUnique  4
+absentConstraintErrorIdKey    = mkPreludeMiscIdUnique  5
 foldrIdKey                    = mkPreludeMiscIdUnique  6
 recSelErrorIdKey              = mkPreludeMiscIdUnique  7
 seqIdKey                      = mkPreludeMiscIdUnique  8
@@ -2330,7 +2350,7 @@ traceKey                      = mkPreludeMiscIdUnique 108
 nospecIdKey :: Unique
 nospecIdKey                   = mkPreludeMiscIdUnique 109
 
-inlineIdKey, noinlineIdKey :: Unique
+inlineIdKey, noinlineIdKey, noinlineConstraintIdKey :: Unique
 inlineIdKey                   = mkPreludeMiscIdUnique 120
 -- see below
 
@@ -2338,8 +2358,9 @@ mapIdKey, dollarIdKey, coercionTokenIdKey, considerAccessibleIdKey :: Unique
 mapIdKey                = mkPreludeMiscIdUnique 121
 dollarIdKey             = mkPreludeMiscIdUnique 123
 coercionTokenIdKey      = mkPreludeMiscIdUnique 124
-noinlineIdKey           = mkPreludeMiscIdUnique 125
-considerAccessibleIdKey = mkPreludeMiscIdUnique 126
+considerAccessibleIdKey = mkPreludeMiscIdUnique 125
+noinlineIdKey           = mkPreludeMiscIdUnique 126
+noinlineConstraintIdKey = mkPreludeMiscIdUnique 127
 
 integerToFloatIdKey, integerToDoubleIdKey, naturalToFloatIdKey, naturalToDoubleIdKey :: Unique
 integerToFloatIdKey    = mkPreludeMiscIdUnique 128
@@ -2479,14 +2500,15 @@ tr'PtrRepLiftedKey     = mkPreludeMiscIdUnique 515
 trLiftedRepKey         = mkPreludeMiscIdUnique 516
 
 -- KindReps for common cases
-starKindRepKey, starArrStarKindRepKey, starArrStarArrStarKindRepKey :: Unique
-starKindRepKey        = mkPreludeMiscIdUnique 520
-starArrStarKindRepKey = mkPreludeMiscIdUnique 521
+starKindRepKey, starArrStarKindRepKey, starArrStarArrStarKindRepKey, constraintKindRepKey :: Unique
+starKindRepKey               = mkPreludeMiscIdUnique 520
+starArrStarKindRepKey        = mkPreludeMiscIdUnique 521
 starArrStarArrStarKindRepKey = mkPreludeMiscIdUnique 522
+constraintKindRepKey         = mkPreludeMiscIdUnique 523
 
 -- Dynamic
 toDynIdKey :: Unique
-toDynIdKey            = mkPreludeMiscIdUnique 523
+toDynIdKey            = mkPreludeMiscIdUnique 530
 
 
 bitIntegerIdKey :: Unique
@@ -2780,9 +2802,10 @@ pretendNameIsInScope n
     [ liftedTypeKindTyConKey, unliftedTypeKindTyConKey
     , liftedDataConKey, unliftedDataConKey
     , tYPETyConKey
+    , cONSTRAINTTyConKey
     , runtimeRepTyConKey, boxedRepDataConKey
     , eqTyConKey
     , listTyConKey
     , oneDataConKey
     , manyDataConKey
-    , funTyConKey ]
+    , fUNTyConKey, unrestrictedFunTyConKey ]

compiler/GHC/Builtin/Types.hs

@@ -34,7 +34,7 @@ module GHC.Builtin.Types (
         promotedLTDataCon, promotedEQDataCon, promotedGTDataCon,
 
         -- * Boxing primitive types
-        boxingDataCon_maybe,
+        boxingDataCon, BoxingInfo(..),
 
         -- * Char
         charTyCon, charDataCon, charTyCon_RDR,
@@ -63,10 +63,6 @@ module GHC.Builtin.Types (
         promotedNilDataCon, promotedConsDataCon,
         mkListTy, mkPromotedListTy,
 
-        -- * NonEmpty
-        nonEmptyTyCon, nonEmptyTyConName,
-        nonEmptyDataCon, nonEmptyDataConName,
-
         -- * Maybe
         maybeTyCon, maybeTyConName,
         nothingDataCon, nothingDataConName, promotedNothingDataCon,
@@ -83,7 +79,7 @@ module GHC.Builtin.Types (
         unboxedUnitTy,
         unboxedUnitTyCon, unboxedUnitDataCon,
         unboxedTupleKind, unboxedSumKind,
-        filterCTuple,
+        filterCTuple, mkConstraintTupleTy,
 
         -- ** Constraint tuples
         cTupleTyCon, cTupleTyConName, cTupleTyConNames, isCTupleTyConName,
@@ -105,6 +101,8 @@ module GHC.Builtin.Types (
         isLiftedTypeKindTyConName,
         typeToTypeKind,
         liftedRepTyCon, unliftedRepTyCon,
+        tYPETyCon, tYPETyConName, tYPEKind,
+        cONSTRAINTTyCon, cONSTRAINTTyConName, cONSTRAINTKind,
         constraintKind, liftedTypeKind, unliftedTypeKind, zeroBitTypeKind,
         constraintKindTyCon, liftedTypeKindTyCon, unliftedTypeKindTyCon,
         constraintKindTyConName, liftedTypeKindTyConName, unliftedTypeKindTyConName,
@@ -116,15 +114,17 @@ module GHC.Builtin.Types (
         coercibleTyCon, coercibleTyConName, coercibleDataCon, coercibleClass,
 
         -- * RuntimeRep and friends
-        runtimeRepTyCon, levityTyCon, vecCountTyCon, vecElemTyCon,
+        runtimeRepTyCon, vecCountTyCon, vecElemTyCon,
 
         boxedRepDataConTyCon,
-        runtimeRepTy, levityTy, liftedRepTy, unliftedRepTy, zeroBitRepTy,
+        runtimeRepTy, liftedRepTy, unliftedRepTy, zeroBitRepTy,
 
         vecRepDataConTyCon, tupleRepDataConTyCon, sumRepDataConTyCon,
 
+        -- * Levity
+        levityTyCon, levityTy,
         liftedDataConTyCon, unliftedDataConTyCon,
-        liftedDataConTy, unliftedDataConTy,
+        liftedDataConTy,    unliftedDataConTy,
 
         intRepDataConTy,
         int8RepDataConTy, int16RepDataConTy, int32RepDataConTy, int64RepDataConTy,
@@ -170,27 +170,32 @@ import GHC.Builtin.Types.Prim
 import GHC.Builtin.Uniques
 
 -- others:
+import GHC.Core( Expr(Type), mkConApp )
 import GHC.Core.Coercion.Axiom
-import GHC.Types.Id
-import GHC.Types.TyThing
-import GHC.Types.SourceText
-import GHC.Types.Var (VarBndr (Bndr))
-import GHC.Settings.Constants ( mAX_TUPLE_SIZE, mAX_CTUPLE_SIZE, mAX_SUM_SIZE )
-import GHC.Unit.Module        ( Module )
 import GHC.Core.Type
-import qualified GHC.Core.TyCo.Rep as TyCoRep (Type(TyConApp))
-import GHC.Core.TyCo.Rep (RuntimeRepType)
-import GHC.Types.RepType
+import GHC.Types.Id
 import GHC.Core.DataCon
 import GHC.Core.ConLike
 import GHC.Core.TyCon
 import GHC.Core.Class     ( Class, mkClass )
+import GHC.Core.Map.Type  ( TypeMap, emptyTypeMap, extendTypeMap, lookupTypeMap )
+import qualified GHC.Core.TyCo.Rep as TyCoRep (Type(TyConApp))
+
+import GHC.Types.TyThing
+import GHC.Types.SourceText
+import GHC.Types.Var ( VarBndr (Bndr) )
+import GHC.Types.RepType
 import GHC.Types.Name.Reader
 import GHC.Types.Name as Name
-import GHC.Types.Name.Env ( NameEnv, mkNameEnv, lookupNameEnv, lookupNameEnv_NF )
+import GHC.Types.Name.Env ( lookupNameEnv_NF )
 import GHC.Types.Basic
 import GHC.Types.ForeignCall
 import GHC.Types.Unique.Set
+
+
+import GHC.Settings.Constants ( mAX_TUPLE_SIZE, mAX_CTUPLE_SIZE, mAX_SUM_SIZE )
+import GHC.Unit.Module        ( Module )
+
 import Data.Array
 import GHC.Data.FastString
 import GHC.Data.BooleanFormula ( mkAnd )
@@ -274,7 +279,8 @@ names in GHC.Builtin.Names, so they use wTcQual, wDataQual, etc
 -- See also Note [Known-key names]
 wiredInTyCons :: [TyCon]
 
-wiredInTyCons = [ -- Units are not treated like other tuples, because they
+wiredInTyCons = map (dataConTyCon . snd) boxingDataCons
+             ++ [ -- Units are not treated like other tuples, because they
                   -- are defined in GHC.Base, and there's only a few of them. We
                   -- put them in wiredInTyCons so that they will pre-populate
                   -- the name cache, so the parser in isBuiltInOcc_maybe doesn't
@@ -318,7 +324,6 @@ wiredInTyCons = [ -- Units are not treated like other tuples, because they
                 , unliftedRepTyCon
                 , zeroBitRepTyCon
                 , zeroBitTypeTyCon
-                , nonEmptyTyCon
                 ]
 
 mkWiredInTyConName :: BuiltInSyntax -> Module -> FastString -> Unique -> TyCon -> Name
@@ -377,10 +382,6 @@ listTyConName     = mkWiredInTyConName   UserSyntax    gHC_TYPES (fsLit "List")
 nilDataConName    = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit "[]") nilDataConKey nilDataCon
 consDataConName   = mkWiredInDataConName BuiltInSyntax gHC_TYPES (fsLit ":") consDataConKey consDataCon
 
-nonEmptyTyConName, nonEmptyDataConName :: Name
-nonEmptyTyConName   = mkWiredInTyConName   UserSyntax  gHC_BASE (fsLit "NonEmpty") nonEmptyTyConKey nonEmptyTyCon
-nonEmptyDataConName = mkWiredInDataConName UserSyntax  gHC_BASE (fsLit ":|") nonEmptyDataConKey nonEmptyDataCon
-
 maybeTyConName, nothingDataConName, justDataConName :: Name
 maybeTyConName     = mkWiredInTyConName   UserSyntax gHC_MAYBE (fsLit "Maybe")
                                           maybeTyConKey maybeTyCon
@@ -509,80 +510,6 @@ makeRecoveryTyCon tc
 typeSymbolKindConName :: Name
 typeSymbolKindConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Symbol") typeSymbolKindConNameKey typeSymbolKindCon
 
-constraintKindTyConName :: Name
-constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constraint") constraintKindTyConKey   constraintKindTyCon
-
-liftedTypeKindTyConName, unliftedTypeKindTyConName, zeroBitTypeTyConName :: Name
-liftedTypeKindTyConName   = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type")         liftedTypeKindTyConKey   liftedTypeKindTyCon
-unliftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedType") unliftedTypeKindTyConKey unliftedTypeKindTyCon
-zeroBitTypeTyConName      = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "ZeroBitType")  zeroBitTypeTyConKey      zeroBitTypeTyCon
-
-liftedRepTyConName, unliftedRepTyConName, zeroBitRepTyConName :: Name
-liftedRepTyConName   = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "LiftedRep")   liftedRepTyConKey   liftedRepTyCon
-unliftedRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedRep") unliftedRepTyConKey unliftedRepTyCon
-zeroBitRepTyConName  = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "ZeroBitRep")  zeroBitRepTyConKey  zeroBitRepTyCon
-
-multiplicityTyConName :: Name
-multiplicityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Multiplicity")
-                          multiplicityTyConKey multiplicityTyCon
-
-oneDataConName, manyDataConName :: Name
-oneDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "One") oneDataConKey oneDataCon
-manyDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Many") manyDataConKey manyDataCon
-
-runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName, boxedRepDataConName :: Name
-runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
-vecRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "VecRep") vecRepDataConKey vecRepDataCon
-tupleRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "TupleRep") tupleRepDataConKey tupleRepDataCon
-sumRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "SumRep") sumRepDataConKey sumRepDataCon
-boxedRepDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "BoxedRep") boxedRepDataConKey boxedRepDataCon
-
-levityTyConName, liftedDataConName, unliftedDataConName :: Name
-levityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Levity") levityTyConKey levityTyCon
-liftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Lifted") liftedDataConKey liftedDataCon
-unliftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Unlifted") unliftedDataConKey unliftedDataCon
-
-
--- See Note [Wiring in RuntimeRep]
-runtimeRepSimpleDataConNames :: [Name]
-runtimeRepSimpleDataConNames
-  = zipWith3Lazy mk_special_dc_name
-      [ fsLit "IntRep"
-      , fsLit "Int8Rep", fsLit "Int16Rep", fsLit "Int32Rep", fsLit "Int64Rep"
-      , fsLit "WordRep"
-      , fsLit "Word8Rep", fsLit "Word16Rep", fsLit "Word32Rep", fsLit "Word64Rep"
-      , fsLit "AddrRep"
-      , fsLit "FloatRep", fsLit "DoubleRep"
-      ]
-      runtimeRepSimpleDataConKeys
-      runtimeRepSimpleDataCons
-
-vecCountTyConName :: Name
-vecCountTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecCount") vecCountTyConKey vecCountTyCon
-
--- See Note [Wiring in RuntimeRep]
-vecCountDataConNames :: [Name]
-vecCountDataConNames = zipWith3Lazy mk_special_dc_name
-                         [ fsLit "Vec2", fsLit "Vec4", fsLit "Vec8"
-                         , fsLit "Vec16", fsLit "Vec32", fsLit "Vec64" ]
-                         vecCountDataConKeys
-                         vecCountDataCons
-
-vecElemTyConName :: Name
-vecElemTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecElem") vecElemTyConKey vecElemTyCon
-
--- See Note [Wiring in RuntimeRep]
-vecElemDataConNames :: [Name]
-vecElemDataConNames = zipWith3Lazy mk_special_dc_name
-                        [ fsLit "Int8ElemRep", fsLit "Int16ElemRep", fsLit "Int32ElemRep"
-                        , fsLit "Int64ElemRep", fsLit "Word8ElemRep", fsLit "Word16ElemRep"
-                        , fsLit "Word32ElemRep", fsLit "Word64ElemRep"
-                        , fsLit "FloatElemRep", fsLit "DoubleElemRep" ]
-                        vecElemDataConKeys
-                        vecElemDataCons
-
-mk_special_dc_name :: FastString -> Unique -> DataCon -> Name
-mk_special_dc_name fs u dc = mkWiredInDataConName UserSyntax gHC_TYPES fs u dc
 
 boolTyCon_RDR, false_RDR, true_RDR, intTyCon_RDR, charTyCon_RDR, stringTyCon_RDR,
     intDataCon_RDR, listTyCon_RDR, consDataCon_RDR :: RdrName
@@ -609,7 +536,7 @@ consDataCon_RDR = nameRdrName consDataConName
 pcTyCon :: Name -> Maybe CType -> [TyVar] -> [DataCon] -> TyCon
 pcTyCon name cType tyvars cons
   = mkAlgTyCon name
-                (mkAnonTyConBinders VisArg tyvars)
+                (mkAnonTyConBinders tyvars)
                 liftedTypeKind
                 (map (const Representational) tyvars)
                 cType
@@ -619,24 +546,41 @@ pcTyCon name cType tyvars cons
                 False           -- Not in GADT syntax
 
 pcDataCon :: Name -> [TyVar] -> [Type] -> TyCon -> DataCon
-pcDataCon n univs tys = pcDataConW n univs (map linear tys)
-
-pcDataConW :: Name -> [TyVar] -> [Scaled Type] -> TyCon -> DataCon
-pcDataConW n univs tys = pcDataConWithFixity False n univs
+pcDataCon n univs tys
+  = pcDataConWithFixity False n univs
                       []    -- no ex_tvs
                       univs -- the univs are precisely the user-written tyvars
-                      tys
+                      []    -- No theta
+                      (map linear tys)
+
+pcDataConConstraint :: Name -> [TyVar] -> ThetaType -> TyCon -> DataCon
+-- Used for data constructors whose arguments are all constraints.
+-- Notably constraint tuples, Eq# etc.
+pcDataConConstraint n univs theta
+  = pcDataConWithFixity False n univs
+                      []    -- No ex_tvs
+                      univs -- The univs are precisely the user-written tyvars
+                      theta -- All constraint arguments
+                      []    -- No value arguments
+
+-- Used for RuntimeRep and friends; things with PromDataConInfo
+pcSpecialDataCon :: Name -> [Type] -> TyCon -> PromDataConInfo -> DataCon
+pcSpecialDataCon dc_name arg_tys tycon rri
+  = pcDataConWithFixity' False dc_name
+                         (dataConWorkerUnique (nameUnique dc_name)) rri
+                         [] [] [] [] (map linear arg_tys) tycon
 
 pcDataConWithFixity :: Bool      -- ^ declared infix?
                     -> Name      -- ^ datacon name
                     -> [TyVar]   -- ^ univ tyvars
                     -> [TyCoVar] -- ^ ex tycovars
                     -> [TyCoVar] -- ^ user-written tycovars
+                    -> ThetaType
                     -> [Scaled Type]    -- ^ args
                     -> TyCon
                     -> DataCon
-pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (nameUnique n))
-                                                  NoRRI
+pcDataConWithFixity infx n = pcDataConWithFixity' infx n
+                                 (dataConWorkerUnique (nameUnique n)) NoPromInfo
 -- The Name's unique is the first of two free uniques;
 -- the first is used for the datacon itself,
 -- the second is used for the "worker name"
@@ -644,9 +588,9 @@ pcDataConWithFixity infx n = pcDataConWithFixity' infx n (dataConWorkerUnique (n
 -- To support this the mkPreludeDataConUnique function "allocates"
 -- one DataCon unique per pair of Ints.
 
-pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
+pcDataConWithFixity' :: Bool -> Name -> Unique -> PromDataConInfo
                      -> [TyVar] -> [TyCoVar] -> [TyCoVar]
-                     -> [Scaled Type] -> TyCon -> DataCon
+                     -> ThetaType -> [Scaled Type] -> TyCon -> DataCon
 -- The Name should be in the DataName name space; it's the name
 -- of the DataCon itself.
 --
@@ -658,7 +602,7 @@ pcDataConWithFixity' :: Bool -> Name -> Unique -> RuntimeRepInfo
 --    to regret doing so (we do).
 
 pcDataConWithFixity' declared_infix dc_name wrk_key rri
-                     tyvars ex_tyvars user_tyvars arg_tys tycon
+                     tyvars ex_tyvars user_tyvars theta arg_tys tycon
   = data_con
   where
     tag_map = mkTyConTagMap tycon
@@ -674,7 +618,7 @@ pcDataConWithFixity' declared_infix dc_name wrk_key rri
                 tyvars ex_tyvars
                 (mkTyVarBinders SpecifiedSpec user_tyvars)
                 []      -- No equality spec
-                []      -- No theta
+                theta
                 arg_tys (mkTyConApp tycon (mkTyVarTys tyvars))
                 rri
                 tycon
@@ -700,16 +644,11 @@ mkDataConWorkerName data_con wrk_key =
     dc_occ  = nameOccName dc_name
     wrk_occ = mkDataConWorkerOcc dc_occ
 
--- used for RuntimeRep and friends
-pcSpecialDataCon :: Name -> [Type] -> TyCon -> RuntimeRepInfo -> DataCon
-pcSpecialDataCon dc_name arg_tys tycon rri
-  = pcDataConWithFixity' False dc_name (dataConWorkerUnique (nameUnique dc_name)) rri
-                         [] [] [] (map linear arg_tys) tycon
 
 {-
 ************************************************************************
 *                                                                      *
-      Kinds
+              Symbol
 *                                                                      *
 ************************************************************************
 -}
@@ -721,13 +660,6 @@ typeSymbolKindCon = pcTyCon typeSymbolKindConName Nothing [] []
 typeSymbolKind :: Kind
 typeSymbolKind = mkTyConTy typeSymbolKindCon
 
-constraintKindTyCon :: TyCon
--- 'TyCon.isConstraintKindCon' assumes that this is an AlgTyCon!
-constraintKindTyCon = pcTyCon constraintKindTyConName Nothing [] []
-
-typeToTypeKind, constraintKind :: Kind
-typeToTypeKind   = liftedTypeKind `mkVisFunTyMany` liftedTypeKind
-constraintKind   = mkTyConTy constraintKindTyCon
 
 {-
 ************************************************************************
@@ -868,7 +800,7 @@ isBuiltInOcc_maybe occ =
       ":"    -> Just consDataConName
 
       -- function tycon
-      "FUN"  -> Just funTyConName
+      "FUN"  -> Just fUNTyConName
       "->"  -> Just unrestrictedFunTyConName
 
       -- boxed tuple data/tycon
@@ -1162,7 +1094,7 @@ mk_ctuple arity = (tycon, tuple_con, sc_sel_ids_arr)
                          (mkPrelTyConRepName tc_name)
 
     klass     = mk_ctuple_class tycon sc_theta sc_sel_ids
-    tuple_con = pcDataConW dc_name tvs (map unrestricted sc_theta) tycon
+    tuple_con = pcDataConConstraint dc_name tvs sc_theta tycon
 
     binders = mkTemplateAnonTyConBinders (replicate arity constraintKind)
     roles   = replicate arity Nominal
@@ -1220,7 +1152,6 @@ unboxedUnitTyCon = tupleTyCon Unboxed 0
 unboxedUnitDataCon :: DataCon
 unboxedUnitDataCon = tupleDataCon Unboxed 0
 
-
 {- *********************************************************************
 *                                                                      *
       Unboxed sums
@@ -1349,7 +1280,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName eqTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataConW eqDataConName tvs [unrestricted sc_pred] tycon
+    datacon   = pcDataConConstraint eqDataConName tvs [sc_pred] tycon
 
     -- Kind: forall k. k -> k -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
@@ -1367,7 +1298,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName heqTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataConW heqDataConName tvs [unrestricted sc_pred] tycon
+    datacon   = pcDataConConstraint heqDataConName tvs [sc_pred] tycon
 
     -- Kind: forall k1 k2. k1 -> k2 -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
@@ -1385,7 +1316,7 @@ eqSCSelId, heqSCSelId, coercibleSCSelId :: Id
                              rhs klass
                              (mkPrelTyConRepName coercibleTyConName)
     klass     = mk_class tycon sc_pred sc_sel_id
-    datacon   = pcDataConW coercibleDataConName tvs [unrestricted sc_pred] tycon
+    datacon   = pcDataConConstraint coercibleDataConName tvs [sc_pred] tycon
 
     -- Kind: forall k. k -> k -> Constraint
     binders   = mkTemplateTyConBinders [liftedTypeKind] (\[k] -> [k,k])
@@ -1419,12 +1350,20 @@ mk_ctuple_class tycon sc_theta sc_sel_ids
 data Multiplicity = One | Many
 -}
 
+multiplicityTyConName :: Name
+multiplicityTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Multiplicity")
+                          multiplicityTyConKey multiplicityTyCon
+
+oneDataConName, manyDataConName :: Name
+oneDataConName  = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "One") oneDataConKey oneDataCon
+manyDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Many") manyDataConKey manyDataCon
+
 multiplicityTy :: Type
 multiplicityTy = mkTyConTy multiplicityTyCon
 
 multiplicityTyCon :: TyCon
 multiplicityTyCon = pcTyCon multiplicityTyConName Nothing []
-                          [oneDataCon, manyDataCon]
+                            [oneDataCon, manyDataCon]
 
 oneDataCon, manyDataCon :: DataCon
 oneDataCon = pcDataCon oneDataConName [] [] multiplicityTyCon
@@ -1450,19 +1389,21 @@ multMulTyCon = mkFamilyTyCon multMulTyConName binders multiplicityTy Nothing
   where
     binders = mkTemplateAnonTyConBinders [multiplicityTy, multiplicityTy]
 
-unrestrictedFunTy :: Type
-unrestrictedFunTy = functionWithMultiplicity manyDataConTy
-
+------------------------
+-- type (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
+--              TYPE rep1 -> TYPE rep2 -> Type
+-- type (->) = FUN 'Many
 unrestrictedFunTyCon :: TyCon
-unrestrictedFunTyCon = buildSynTyCon unrestrictedFunTyConName [] arrowKind [] unrestrictedFunTy
-  where arrowKind = mkTyConKind binders liftedTypeKind
-        -- See also funTyCon
-        binders = [ Bndr runtimeRep1TyVar (NamedTCB Inferred)
-                  , Bndr runtimeRep2TyVar (NamedTCB Inferred)
-                  ]
-                  ++ mkTemplateAnonTyConBinders [ mkTYPEapp runtimeRep1Ty
-                                                , mkTYPEapp runtimeRep2Ty
-                                                ]
+unrestrictedFunTyCon
+  = buildSynTyCon unrestrictedFunTyConName [] arrowKind []
+                  (TyCoRep.TyConApp fUNTyCon [manyDataConTy])
+  where
+    arrowKind = mkTyConKind binders liftedTypeKind
+    -- See also funTyCon
+    binders = [ Bndr runtimeRep1TyVar (NamedTCB Inferred)
+              , Bndr runtimeRep2TyVar (NamedTCB Inferred) ]
+              ++ mkTemplateAnonTyConBinders [ mkTYPEapp runtimeRep1Ty
+                                            , mkTYPEapp runtimeRep2Ty ]
 
 unrestrictedFunTyConName :: Name
 unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->")
@@ -1473,84 +1414,82 @@ unrestrictedFunTyConName = mkWiredInTyConName BuiltInSyntax gHC_TYPES (fsLit "->
 *                                                                      *
       Type synonyms (all declared in ghc-prim:GHC.Types)
 
-         type Type         = TYPE LiftedRep    -- liftedTypeKind
-         type UnliftedType = TYPE UnliftedRep  -- unliftedTypeKind
-         type LiftedRep    = BoxedRep Lifted   -- liftedRepTy
-         type UnliftedRep  = BoxedRep Unlifted -- unliftedRepTy
+         type CONSTRAINT   :: RuntimeRep -> Type -- primitive; cONSTRAINTKind
+         type Constraint   = CONSTRAINT LiftedRep  :: Type    -- constraintKind
+
+         type TYPE         :: RuntimeRep -> Type  -- primitive; tYPEKind
+         type Type         = TYPE LiftedRep   :: Type         -- liftedTypeKind
+         type UnliftedType = TYPE UnliftedRep :: Type         -- unliftedTypeKind
+
+         type LiftedRep    = BoxedRep Lifted   :: RuntimeRep  -- liftedRepTy
+         type UnliftedRep  = BoxedRep Unlifted :: RuntimeRep  -- unliftedRepTy
 
 *                                                                      *
 ********************************************************************* -}
 
 -- For these synonyms, see
--- Note [TYPE and RuntimeRep] in GHC.Builtin.Types.Prim, and
+-- Note [TYPE and CONSTRAINT] in GHC.Builtin.Types.Prim, and
 -- Note [Using synonyms to compress types] in GHC.Core.Type
 
+{- Note [Naked FunTy]
+~~~~~~~~~~~~~~~~~~~~~
+GHC.Core.TyCo.Rep.mkFunTy has assertions about the consistency of the argument
+flag and arg/res types.  But when constructing the kinds of tYPETyCon and
+cONSTRAINTTyCon we don't want to make these checks because
+     TYPE :: RuntimeRep -> Type
+i.e. TYPE :: RuntimeRep -> TYPE LiftedRep
+
+so the check will loop infinitely.  Hence the use of a naked FunTy
+constructor in tTYPETyCon and cONSTRAINTTyCon.
+-}
+
+
+----------------------
+-- type Constraint = CONSTRAINT LiftedRep
+constraintKindTyCon :: TyCon
+constraintKindTyCon
+  = buildSynTyCon constraintKindTyConName [] liftedTypeKind [] rhs
+  where
+    rhs = TyCoRep.TyConApp cONSTRAINTTyCon [liftedRepTy]
+
+constraintKindTyConName :: Name
+constraintKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Constraint")
+                                             constraintKindTyConKey constraintKindTyCon
+
+constraintKind :: Kind
+constraintKind = mkTyConTy constraintKindTyCon
+
 ----------------------
--- @type Type = TYPE ('BoxedRep 'Lifted)@
+-- type Type = TYPE LiftedRep
 liftedTypeKindTyCon :: TyCon
 liftedTypeKindTyCon
   = buildSynTyCon liftedTypeKindTyConName [] liftedTypeKind [] rhs
   where
     rhs = TyCoRep.TyConApp tYPETyCon [liftedRepTy]
 
-liftedTypeKind :: Type
+liftedTypeKindTyConName :: Name
+liftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "Type")
+                                             liftedTypeKindTyConKey liftedTypeKindTyCon
+
+liftedTypeKind, typeToTypeKind :: Type
 liftedTypeKind = mkTyConTy liftedTypeKindTyCon
+typeToTypeKind = liftedTypeKind `mkVisFunTyMany` liftedTypeKind
 
 ----------------------
--- | @type UnliftedType = TYPE ('BoxedRep 'Unlifted)@
+-- type UnliftedType = TYPE ('BoxedRep 'Unlifted)
 unliftedTypeKindTyCon :: TyCon
 unliftedTypeKindTyCon
   = buildSynTyCon unliftedTypeKindTyConName [] liftedTypeKind [] rhs
   where
     rhs = TyCoRep.TyConApp tYPETyCon [unliftedRepTy]
 
+unliftedTypeKindTyConName :: Name
+unliftedTypeKindTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedType")
+                                                unliftedTypeKindTyConKey unliftedTypeKindTyCon
+
 unliftedTypeKind :: Type
 unliftedTypeKind = mkTyConTy unliftedTypeKindTyCon
 
-----------------------
--- @type ZeroBitType = TYPE ZeroBitRep
-zeroBitTypeTyCon :: TyCon
-zeroBitTypeTyCon
-  = buildSynTyCon zeroBitTypeTyConName [] liftedTypeKind [] rhs
-  where
-    rhs = TyCoRep.TyConApp tYPETyCon [zeroBitRepTy]
-
-zeroBitTypeKind :: Type
-zeroBitTypeKind = mkTyConTy zeroBitTypeTyCon
-
-----------------------
--- | @type LiftedRep = 'BoxedRep 'Lifted@
-liftedRepTyCon :: TyCon
-liftedRepTyCon
-  = buildSynTyCon liftedRepTyConName [] runtimeRepTy [] rhs
-  where
-    rhs = TyCoRep.TyConApp boxedRepDataConTyCon [liftedDataConTy]
-
-liftedRepTy :: RuntimeRepType
-liftedRepTy = mkTyConTy liftedRepTyCon
-
-----------------------
--- | @type UnliftedRep = 'BoxedRep 'Unlifted@
-unliftedRepTyCon :: TyCon
-unliftedRepTyCon
-  = buildSynTyCon unliftedRepTyConName [] runtimeRepTy [] rhs
-  where
-    rhs = TyCoRep.TyConApp boxedRepDataConTyCon [unliftedDataConTy]
-
-unliftedRepTy :: RuntimeRepType
-unliftedRepTy = mkTyConTy unliftedRepTyCon
-
-----------------------
--- | @type ZeroBitRep = 'Tuple '[]
-zeroBitRepTyCon :: TyCon
-zeroBitRepTyCon
-  = buildSynTyCon zeroBitRepTyConName [] runtimeRepTy [] rhs
-  where
-    rhs = TyCoRep.TyConApp tupleRepDataConTyCon [mkPromotedListTy runtimeRepTy []]
-
-zeroBitRepTy :: RuntimeRepType
-zeroBitRepTy = mkTyConTy zeroBitRepTyCon
-
 
 {- *********************************************************************
 *                                                                      *
@@ -1558,6 +1497,11 @@ zeroBitRepTy = mkTyConTy zeroBitRepTyCon
 *                                                                      *
 ********************************************************************* -}
 
+levityTyConName, liftedDataConName, unliftedDataConName :: Name
+levityTyConName     = mkWiredInTyConName   UserSyntax gHC_TYPES (fsLit "Levity")   levityTyConKey     levityTyCon
+liftedDataConName   = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Lifted")   liftedDataConKey   liftedDataCon
+unliftedDataConName = mkWiredInDataConName UserSyntax gHC_TYPES (fsLit "Unlifted") unliftedDataConKey unliftedDataCon
+
 levityTyCon :: TyCon
 levityTyCon = pcTyCon levityTyConName Nothing [] [liftedDataCon,unliftedDataCon]
 
@@ -1566,9 +1510,9 @@ levityTy = mkTyConTy levityTyCon
 
 liftedDataCon, unliftedDataCon :: DataCon
 liftedDataCon = pcSpecialDataCon liftedDataConName
-    [] levityTyCon LiftedInfo
+    [] levityTyCon (Levity Lifted)
 unliftedDataCon = pcSpecialDataCon unliftedDataConName
-    [] levityTyCon UnliftedInfo
+    [] levityTyCon (Levity Unlifted)
 
 liftedDataConTyCon :: TyCon
 liftedDataConTyCon = promoteDataCon liftedDataCon
@@ -1608,21 +1552,35 @@ See also Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType.
 
 runtimeRepTyCon :: TyCon
 runtimeRepTyCon = pcTyCon runtimeRepTyConName Nothing []
+    -- Here we list all the data constructors
+    -- of the RuntimeRep data type
     (vecRepDataCon : tupleRepDataCon :
-     sumRepDataCon : boxedRepDataCon : runtimeRepSimpleDataCons)
+     sumRepDataCon : boxedRepDataCon :
+     runtimeRepSimpleDataCons)
 
 runtimeRepTy :: Type
 runtimeRepTy = mkTyConTy runtimeRepTyCon
 
+runtimeRepTyConName, vecRepDataConName, tupleRepDataConName, sumRepDataConName, boxedRepDataConName :: Name
+runtimeRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "RuntimeRep") runtimeRepTyConKey runtimeRepTyCon
+
+vecRepDataConName   = mk_runtime_rep_dc_name (fsLit "VecRep")   vecRepDataConKey   vecRepDataCon
+tupleRepDataConName = mk_runtime_rep_dc_name (fsLit "TupleRep") tupleRepDataConKey tupleRepDataCon
+sumRepDataConName   = mk_runtime_rep_dc_name (fsLit "SumRep")   sumRepDataConKey   sumRepDataCon
+boxedRepDataConName = mk_runtime_rep_dc_name (fsLit "BoxedRep") boxedRepDataConKey boxedRepDataCon
+
+mk_runtime_rep_dc_name :: FastString -> Unique -> DataCon -> Name
+mk_runtime_rep_dc_name fs u dc = mkWiredInDataConName UserSyntax gHC_TYPES fs u dc
+
 boxedRepDataCon :: DataCon
 boxedRepDataCon = pcSpecialDataCon boxedRepDataConName
   [ levityTy ] runtimeRepTyCon (RuntimeRep prim_rep_fun)
   where
     -- See Note [Getting from RuntimeRep to PrimRep] in RepType
     prim_rep_fun [lev]
-      = case tyConRuntimeRepInfo (tyConAppTyCon lev) of
-          LiftedInfo -> [LiftedRep]
-          UnliftedInfo -> [UnliftedRep]
+      = case tyConPromDataConInfo (tyConAppTyCon lev) of
+          Levity Lifted   -> [LiftedRep]
+          Levity Unlifted -> [UnliftedRep]
           _ -> pprPanic "boxedRepDataCon" (ppr lev)
     prim_rep_fun args
       = pprPanic "boxedRepDataCon" (ppr args)
@@ -1631,23 +1589,6 @@ boxedRepDataCon = pcSpecialDataCon boxedRepDataConName
 boxedRepDataConTyCon :: TyCon
 boxedRepDataConTyCon = promoteDataCon boxedRepDataCon
 
-vecRepDataCon :: DataCon
-vecRepDataCon = pcSpecialDataCon vecRepDataConName [ mkTyConTy vecCountTyCon
-                                                   , mkTyConTy vecElemTyCon ]
-                                 runtimeRepTyCon
-                                 (RuntimeRep prim_rep_fun)
-  where
-    -- See Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType
-    prim_rep_fun [count, elem]
-      | VecCount n <- tyConRuntimeRepInfo (tyConAppTyCon count)
-      , VecElem  e <- tyConRuntimeRepInfo (tyConAppTyCon elem)
-      = [VecRep n e]
-    prim_rep_fun args
-      = pprPanic "vecRepDataCon" (ppr args)
-
-vecRepDataConTyCon :: TyCon
-vecRepDataConTyCon = promoteDataCon vecRepDataCon
-
 tupleRepDataCon :: DataCon
 tupleRepDataCon = pcSpecialDataCon tupleRepDataConName [ mkListTy runtimeRepTy ]
                                    runtimeRepTyCon (RuntimeRep prim_rep_fun)
@@ -1685,18 +1626,27 @@ sumRepDataConTyCon = promoteDataCon sumRepDataCon
 -- See Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType
 runtimeRepSimpleDataCons :: [DataCon]
 runtimeRepSimpleDataCons
-  = zipWithLazy mk_runtime_rep_dc
-    [ IntRep
-    , Int8Rep, Int16Rep, Int32Rep, Int64Rep
-    , WordRep
-    , Word8Rep, Word16Rep, Word32Rep, Word64Rep
-    , AddrRep
-    , FloatRep, DoubleRep
-    ]
-    runtimeRepSimpleDataConNames
+  = zipWith mk_runtime_rep_dc runtimeRepSimpleDataConKeys
+            [ (fsLit "IntRep",    IntRep)
+            , (fsLit "Int8Rep",   Int8Rep)
+            , (fsLit "Int16Rep",  Int16Rep)
+            , (fsLit "Int32Rep",  Int32Rep)
+            , (fsLit "Int64Rep",  Int64Rep)
+            , (fsLit "WordRep",   WordRep)
+            , (fsLit "Word8Rep",  Word8Rep)
+            , (fsLit "Word16Rep", Word16Rep)
+            , (fsLit "Word32Rep", Word32Rep)
+            , (fsLit "Word64Rep", Word64Rep)
+            , (fsLit "AddrRep",   AddrRep)
+            , (fsLit "FloatRep",  FloatRep)
+            , (fsLit "DoubleRep", DoubleRep) ]
   where
-    mk_runtime_rep_dc primrep name
-      = pcSpecialDataCon name [] runtimeRepTyCon (RuntimeRep (\_ -> [primrep]))
+    mk_runtime_rep_dc :: Unique -> (FastString, PrimRep) -> DataCon
+    mk_runtime_rep_dc uniq (fs, primrep)
+      = data_con
+      where
+        data_con = pcSpecialDataCon dc_name [] runtimeRepTyCon (RuntimeRep (\_ -> [primrep]))
+        dc_name  = mk_runtime_rep_dc_name fs uniq data_con
 
 -- See Note [Wiring in RuntimeRep]
 intRepDataConTy,
@@ -1714,6 +1664,114 @@ intRepDataConTy,
    ]
   = map (mkTyConTy . promoteDataCon) runtimeRepSimpleDataCons
 
+----------------------
+-- | @type ZeroBitRep = 'Tuple '[]
+zeroBitRepTyCon :: TyCon
+zeroBitRepTyCon
+  = buildSynTyCon zeroBitRepTyConName [] runtimeRepTy [] rhs
+  where
+    rhs = TyCoRep.TyConApp tupleRepDataConTyCon [mkPromotedListTy runtimeRepTy []]
+
+zeroBitRepTyConName :: Name
+zeroBitRepTyConName  = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "ZeroBitRep")
+                                          zeroBitRepTyConKey  zeroBitRepTyCon
+
+zeroBitRepTy :: RuntimeRepType
+zeroBitRepTy = mkTyConTy zeroBitRepTyCon
+
+----------------------
+-- @type ZeroBitType = TYPE ZeroBitRep
+zeroBitTypeTyCon :: TyCon
+zeroBitTypeTyCon
+  = buildSynTyCon zeroBitTypeTyConName [] liftedTypeKind [] rhs
+  where
+    rhs = TyCoRep.TyConApp tYPETyCon [zeroBitRepTy]
+
+zeroBitTypeTyConName :: Name
+zeroBitTypeTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "ZeroBitType")
+                                          zeroBitTypeTyConKey zeroBitTypeTyCon
+
+zeroBitTypeKind :: Type
+zeroBitTypeKind = mkTyConTy zeroBitTypeTyCon
+
+----------------------
+-- | @type LiftedRep = 'BoxedRep 'Lifted@
+liftedRepTyCon :: TyCon
+liftedRepTyCon
+  = buildSynTyCon liftedRepTyConName [] runtimeRepTy [] rhs
+  where
+    rhs = TyCoRep.TyConApp boxedRepDataConTyCon [liftedDataConTy]
+
+liftedRepTyConName :: Name
+liftedRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "LiftedRep")
+                                        liftedRepTyConKey liftedRepTyCon
+
+liftedRepTy :: RuntimeRepType
+liftedRepTy = mkTyConTy liftedRepTyCon
+
+----------------------
+-- | @type UnliftedRep = 'BoxedRep 'Unlifted@
+unliftedRepTyCon :: TyCon
+unliftedRepTyCon
+  = buildSynTyCon unliftedRepTyConName [] runtimeRepTy [] rhs
+  where
+    rhs = TyCoRep.TyConApp boxedRepDataConTyCon [unliftedDataConTy]
+
+unliftedRepTyConName :: Name
+unliftedRepTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "UnliftedRep")
+                                          unliftedRepTyConKey unliftedRepTyCon
+
+unliftedRepTy :: RuntimeRepType
+unliftedRepTy = mkTyConTy unliftedRepTyCon
+
+
+{- *********************************************************************
+*                                                                      *
+         VecCount, VecElem
+*                                                                      *
+********************************************************************* -}
+
+vecCountTyConName :: Name
+vecCountTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecCount") vecCountTyConKey vecCountTyCon
+
+-- See Note [Wiring in RuntimeRep]
+vecCountDataConNames :: [Name]
+vecCountDataConNames = zipWith3Lazy mk_runtime_rep_dc_name
+                         [ fsLit "Vec2", fsLit "Vec4", fsLit "Vec8"
+                         , fsLit "Vec16", fsLit "Vec32", fsLit "Vec64" ]
+                         vecCountDataConKeys
+                         vecCountDataCons
+
+vecElemTyConName :: Name
+vecElemTyConName = mkWiredInTyConName UserSyntax gHC_TYPES (fsLit "VecElem") vecElemTyConKey vecElemTyCon
+
+-- See Note [Wiring in RuntimeRep]
+vecElemDataConNames :: [Name]
+vecElemDataConNames = zipWith3Lazy mk_runtime_rep_dc_name
+                        [ fsLit "Int8ElemRep", fsLit "Int16ElemRep", fsLit "Int32ElemRep"
+                        , fsLit "Int64ElemRep", fsLit "Word8ElemRep", fsLit "Word16ElemRep"
+                        , fsLit "Word32ElemRep", fsLit "Word64ElemRep"
+                        , fsLit "FloatElemRep", fsLit "DoubleElemRep" ]
+                        vecElemDataConKeys
+                        vecElemDataCons
+
+vecRepDataCon :: DataCon
+vecRepDataCon = pcSpecialDataCon vecRepDataConName [ mkTyConTy vecCountTyCon
+                                                   , mkTyConTy vecElemTyCon ]
+                                 runtimeRepTyCon
+                                 (RuntimeRep prim_rep_fun)
+  where
+    -- See Note [Getting from RuntimeRep to PrimRep] in GHC.Types.RepType
+    prim_rep_fun [count, elem]
+      | VecCount n <- tyConPromDataConInfo (tyConAppTyCon count)
+      , VecElem  e <- tyConPromDataConInfo (tyConAppTyCon elem)
+      = [VecRep n e]
+    prim_rep_fun args
+      = pprPanic "vecRepDataCon" (ppr args)
+
+vecRepDataConTyCon :: TyCon
+vecRepDataConTyCon = promoteDataCon vecRepDataCon
+
 vecCountTyCon :: TyCon
 vecCountTyCon = pcTyCon vecCountTyConName Nothing [] vecCountDataCons
 
@@ -1763,30 +1821,6 @@ int8ElemRepDataConTy, int16ElemRepDataConTy, int32ElemRepDataConTy,
 *                                                                      *
 ********************************************************************* -}
 
-boxingDataCon_maybe :: TyCon -> Maybe DataCon
---    boxingDataCon_maybe Char# = C#
---    boxingDataCon_maybe Int#  = I#
---    ... etc ...
--- See Note [Boxing primitive types]
-boxingDataCon_maybe tc
-  = lookupNameEnv boxing_constr_env (tyConName tc)
-
-boxing_constr_env :: NameEnv DataCon
-boxing_constr_env
-  = mkNameEnv [(charPrimTyConName  , charDataCon  )
-              ,(intPrimTyConName   , intDataCon   )
-              ,(wordPrimTyConName  , wordDataCon  )
-              ,(floatPrimTyConName , floatDataCon )
-              ,(doublePrimTyConName, doubleDataCon) ]
-
-{- Note [Boxing primitive types]
-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-For a handful of primitive types (Int, Char, Word, Float, Double),
-we can readily box and an unboxed version (Int#, Char# etc) using
-the corresponding data constructor.  This is useful in a couple
-of places, notably let-floating -}
-
-
 charTy :: Type
 charTy = mkTyConTy charTyCon
 
@@ -1863,6 +1897,139 @@ doubleTyCon = pcTyCon doubleTyConName
 doubleDataCon :: DataCon
 doubleDataCon = pcDataCon doubleDataConName [] [doublePrimTy] doubleTyCon
 
+{- *********************************************************************
+*                                                                      *
+              Boxing data constructors
+*                                                                      *
+********************************************************************* -}
+
+{- Note [Boxing constructors]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+In ghc-prim:GHC.Types we have a family of data types, one for each RuntimeRep
+that "box" unlifted values into a (boxed, lifted) value of kind Type. For example
+
+  type Int8Box :: TYPE Int8Rep -> Type
+  data Int8Box (a :: TYPE Int8Rep) = MkInt8Box a
+    -- MkInt8Box :: forall (a :: TYPE Int8Rep). a -> Int8Box a
+
+Then we can package an `Int8#` into an `Int8Box` with `MkInt8Box`.  We can also
+package up a (lifted) Constraint as a value of kind Type.
+
+There are a fixed number of RuntimeReps, so we only need a fixed number
+of boxing types.  (For TupleRep we need to box recursively; not yet done.)
+
+This is used:
+
+* In desugaring, when we need to package up a bunch of values into a tuple,
+  for example when desugaring arrows.  See Note [Big tuples] in GHC.Core.Make.
+
+* In let-floating when we want to float an unlifted sub-expression.
+  See Note [Floating MFEs of unlifted type] in GHC.Core.Opt.SetLevels
+
+In this module we make wired-in data type declarations for all of
+these boxing functions.  The goal is to define boxingDataCon_maybe.
+
+Wrinkles
+(W1) The runtime system has special treatment (e.g. commoning up during GC)
+     for Int and Char values. See  Note [CHARLIKE and INTLIKE closures] and
+     Note [Precomputed static closures] in the RTS.
+
+     So we treat Int# and Char# specially, in specialBoxingDataCon_maybe
+-}
+
+data BoxingInfo b
+  = BI_NoBoxNeeded   -- The type has kind Type, so there is nothing to do
+
+  | BI_NoBoxAvailable  -- The type does not have kind Type, but sadly we
+                       -- don't have a boxing data constructor either
+
+  | BI_Box             -- The type does not have kind Type, and we do have a
+                       -- boxing data constructor; here it is
+      { bi_data_con   :: DataCon
+      , bi_inst_con   :: Expr b
+      , bi_boxed_type :: Type }
+    -- e.g. BI_Box { bi_data_con = I#, bi_inst_con = I#, bi_boxed_type = Int }
+    --        recall: data Int = I# Int#
+    --
+    --      BI_Box { bi_data_con = MkInt8Box, bi_inst_con = MkInt8Box @ty
+    --             , bi_boxed_type = Int8Box ty }A
+    --        recall: data Int8Box (a :: TYPE Int8Rep) = MkIntBox a
+
+boxingDataCon :: Type -> BoxingInfo b
+-- ^ Given a type 'ty', if 'ty' is not of kind Type, return a data constructor that
+--   will box it, and the type of the boxed thing, which /does/ now have kind Type.
+-- See Note [Boxing constructors]
+boxingDataCon ty
+  | tcIsLiftedTypeKind kind
+  = BI_NoBoxNeeded    -- Fast path for Type
+
+  | Just box_con <- specialBoxingDataCon_maybe ty
+  = BI_Box { bi_data_con = box_con, bi_inst_con = mkConApp box_con []
+           , bi_boxed_type = tyConNullaryTy (dataConTyCon box_con) }
+
+  | Just box_con <- lookupTypeMap boxingDataConMap kind
+  = BI_Box { bi_data_con = box_con, bi_inst_con = mkConApp box_con [Type ty]
+           , bi_boxed_type = mkTyConApp (dataConTyCon box_con) [ty] }
+
+  | otherwise
+  = BI_NoBoxAvailable
+
+  where
+    kind = typeKind ty
+
+specialBoxingDataCon_maybe :: Type -> Maybe DataCon
+-- ^ See Note [Boxing constructors] wrinkle (W1)
+specialBoxingDataCon_maybe ty
+  = case splitTyConApp_maybe ty of
+      Just (tc, _) | tc `hasKey` intPrimTyConKey  -> Just intDataCon
+                   | tc `hasKey` charPrimTyConKey -> Just charDataCon
+      _ -> Nothing
+
+boxingDataConMap :: TypeMap DataCon
+-- See Note [Boxing constructors]
+boxingDataConMap = foldl add emptyTypeMap boxingDataCons
+  where
+    add bdcm (kind, boxing_con) = extendTypeMap bdcm kind boxing_con
+
+boxingDataCons :: [(Kind, DataCon)]
+-- The Kind is the kind of types for which the DataCon is the right boxing
+boxingDataCons = zipWith mkBoxingDataCon
+  (map mkBoxingTyConUnique [1..])
+  [ (mkTYPEapp wordRepDataConTy, fsLit "WordBox", fsLit "MkWordBox")
+  , (mkTYPEapp intRepDataConTy,  fsLit "IntBox",  fsLit "MkIntBox")
+
+  , (mkTYPEapp floatRepDataConTy,  fsLit "FloatBox",  fsLit "MkFloatBox")
+  , (mkTYPEapp doubleRepDataConTy,  fsLit "DoubleBox",  fsLit "MkDoubleBox")
+
+  , (mkTYPEapp int8RepDataConTy,  fsLit "Int8Box",  fsLit "MkInt8Box")
+  , (mkTYPEapp int16RepDataConTy, fsLit "Int16Box", fsLit "MkInt16Box")
+  , (mkTYPEapp int32RepDataConTy, fsLit "Int32Box", fsLit "MkInt32Box")
+  , (mkTYPEapp int64RepDataConTy, fsLit "Int64Box", fsLit "MkInt64Box")
+
+  , (mkTYPEapp word8RepDataConTy,  fsLit "Word8Box",   fsLit "MkWord8Box")
+  , (mkTYPEapp word16RepDataConTy, fsLit "Word16Box",  fsLit "MkWord16Box")
+  , (mkTYPEapp word32RepDataConTy, fsLit "Word32Box",  fsLit "MkWord32Box")
+  , (mkTYPEapp word64RepDataConTy, fsLit "Word64Box",  fsLit "MkWord64Box")
+
+  , (unliftedTypeKind, fsLit "LiftBox", fsLit "MkLiftBox")
+  , (constraintKind,   fsLit "DictBox", fsLit "MkDictBox") ]
+
+mkBoxingDataCon :: Unique -> (Kind, FastString, FastString) -> (Kind, DataCon)
+mkBoxingDataCon uniq_tc (kind, fs_tc, fs_dc)
+  = (kind, dc)
+  where
+    uniq_dc = boxingDataConUnique uniq_tc
+
+    (tv:_) = mkTemplateTyVars (repeat kind)
+    tc = pcTyCon tc_name Nothing [tv] [dc]
+    tc_name = mkWiredInTyConName UserSyntax gHC_TYPES fs_tc uniq_tc tc
+
+    dc | isConstraintKind kind
+       = pcDataConConstraint dc_name [tv] [mkTyVarTy tv] tc
+       | otherwise
+       = pcDataCon           dc_name [tv] [mkTyVarTy tv] tc
+    dc_name = mkWiredInDataConName UserSyntax gHC_TYPES fs_dc uniq_dc dc
+
 {-
 ************************************************************************
 *                                                                      *
@@ -1969,23 +2136,14 @@ nilDataCon  = pcDataCon nilDataConName alpha_tyvar [] listTyCon
 consDataCon :: DataCon
 consDataCon = pcDataConWithFixity True {- Declared infix -}
                consDataConName
-               alpha_tyvar [] alpha_tyvar
-               (map linear [alphaTy, mkTyConApp listTyCon alpha_ty]) listTyCon
+               alpha_tyvar [] alpha_tyvar []
+               (map linear [alphaTy, mkTyConApp listTyCon alpha_ty])
+               listTyCon
+
 -- Interesting: polymorphic recursion would help here.
 -- We can't use (mkListTy alphaTy) in the defn of consDataCon, else mkListTy
 -- gets the over-specific type (Type -> Type)
 
--- NonEmpty lists (used for 'ProjectionE')
-nonEmptyTyCon :: TyCon
-nonEmptyTyCon = pcTyCon nonEmptyTyConName Nothing [alphaTyVar] [nonEmptyDataCon]
-
-nonEmptyDataCon :: DataCon
-nonEmptyDataCon = pcDataConWithFixity True {- Declared infix -}
-                    nonEmptyDataConName
-                    alpha_tyvar [] alpha_tyvar
-                    (map linear [alphaTy, mkTyConApp listTyCon alpha_ty])
-                    nonEmptyTyCon
-
 -- Wired-in type Maybe
 
 maybeTyCon :: TyCon
@@ -2075,7 +2233,7 @@ mkTupleTy boxity  tys  = mkTupleTy1 boxity tys
 mkTupleTy1 :: Boxity -> [Type] -> Type
 mkTupleTy1 Boxed   tys  = mkTyConApp (tupleTyCon Boxed (length tys)) tys
 mkTupleTy1 Unboxed tys  = mkTyConApp (tupleTyCon Unboxed (length tys))
-                                         (map getRuntimeRep tys ++ tys)
+                                     (map getRuntimeRep tys ++ tys)
 
 -- | Build the type of a small tuple that holds the specified type of thing
 -- Flattens 1-tuples. See Note [One-tuples].
@@ -2085,6 +2243,18 @@ mkBoxedTupleTy tys = mkTupleTy Boxed tys
 unitTy :: Type
 unitTy = mkTupleTy Boxed []
 
+-- Make a constraint tuple, flattening a 1-tuple as usual
+-- If we get a constraint tuple that is bigger than the pre-built
+--   ones (in ghc-prim:GHC.Tuple), then just make one up anyway; it won't
+--   have an info table in the RTS, so we can't use it at runtime.  But
+--   this is used only in filling in extra-constraint wildcards, so it
+--   never is used at runtime anyway
+--   See GHC.Tc.Gen.HsType Note [Extra-constraint holes in partial type signatures]
+mkConstraintTupleTy :: [Type] -> Type
+mkConstraintTupleTy [ty] = ty
+mkConstraintTupleTy tys = mkTyConApp (cTupleTyCon (length tys)) tys
+
+
 {- *********************************************************************
 *                                                                      *
             The sum types

compiler/GHC/Builtin/Types.hs-boot

@@ -16,8 +16,8 @@ coercibleTyCon, heqTyCon :: TyCon
 
 unitTy :: Type
 
-
 liftedTypeKindTyConName :: Name
+constraintKindTyConName :: Name
 
 liftedTypeKind, unliftedTypeKind, zeroBitTypeKind :: Kind
 

compiler/GHC/Builtin/Types/Literals.hs

@@ -29,12 +29,12 @@ import GHC.Prelude
 
 import GHC.Core.Type
 import GHC.Data.Pair
-import GHC.Tc.Utils.TcType ( TcType, tcEqType )
 import GHC.Core.TyCon    ( TyCon, FamTyConFlav(..), mkFamilyTyCon
                          , Injectivity(..) )
 import GHC.Core.Coercion ( Role(..) )
 import GHC.Tc.Types.Constraint ( Xi )
 import GHC.Core.Coercion.Axiom ( CoAxiomRule(..), BuiltInSynFamily(..), TypeEqn )
+import GHC.Core.TyCo.Compare   ( tcEqType )
 import GHC.Types.Name          ( Name, BuiltInSyntax(..) )
 import GHC.Types.Unique.FM
 import GHC.Builtin.Types
@@ -630,7 +630,7 @@ isOrderingLitTy tc =
          | tc1 == promotedGTDataCon -> return GT
          | otherwise                -> Nothing
 
-known :: (Integer -> Bool) -> TcType -> Bool
+known :: (Integer -> Bool) -> Type -> Bool
 known p x = case isNumLitTy x of
               Just a  -> p a
               Nothing -> False

compiler/GHC/Builtin/Types/Prim.hs

@@ -30,6 +30,8 @@ module GHC.Builtin.Types.Prim(
         levity1TyVarInf, levity2TyVarInf,
         levity1Ty, levity2Ty,
 
+        alphaConstraintTyVar, alphaConstraintTy,
+
         openAlphaTyVar, openBetaTyVar, openGammaTyVar,
         openAlphaTyVarSpec, openBetaTyVarSpec, openGammaTyVarSpec,
         openAlphaTy, openBetaTy, openGammaTy,
@@ -41,13 +43,16 @@ module GHC.Builtin.Types.Prim(
         multiplicityTyVar1, multiplicityTyVar2,
 
         -- Kind constructors...
-        tYPETyCon, tYPETyConName,
+        tYPETyCon, tYPETyConName, tYPEKind,
+        cONSTRAINTTyCon, cONSTRAINTTyConName, cONSTRAINTKind,
 
-        -- Kinds
-        mkTYPEapp,
+        -- Arrows
+        funTyFlagTyCon, isArrowTyCon,
+        fUNTyCon,       fUNTyConName,
+        ctArrowTyCon, ctArrowTyConName,
+        ccArrowTyCon, ccArrowTyConName,
+        tcArrowTyCon, tcArrowTyConName,
 
-        functionWithMultiplicity,
-        funTyCon, funTyConName,
         unexposedPrimTyCons, exposedPrimTyCons, primTyCons,
 
         charPrimTyCon,          charPrimTy, charPrimTyConName,
@@ -121,32 +126,108 @@ import {-# SOURCE #-} GHC.Builtin.Types
   , int64ElemRepDataConTy, word8ElemRepDataConTy, word16ElemRepDataConTy
   , word32ElemRepDataConTy, word64ElemRepDataConTy, floatElemRepDataConTy
   , doubleElemRepDataConTy
-  , multiplicityTy )
+  , multiplicityTy
+  , constraintKind )
+
+import {-# SOURCE #-} GHC.Types.TyThing( mkATyCon )
+import {-# SOURCE #-} GHC.Core.Type ( mkTyConApp, getLevity )
+
+import GHC.Core.TyCon
+import GHC.Core.TyCo.Rep -- Doesn't need special access, but this is easier to avoid
+                         -- import loops which show up if you import Type instead
 
-import GHC.Types.Var    ( TyVarBinder, TyVar
+import GHC.Types.Var    ( TyVarBinder, TyVar,binderVar, binderVars
                         , mkTyVar, mkTyVarBinder, mkTyVarBinders )
 import GHC.Types.Name
-import {-# SOURCE #-} GHC.Types.TyThing
-import GHC.Core.TyCon
 import GHC.Types.SrcLoc
 import GHC.Types.Unique
+
 import GHC.Builtin.Uniques
 import GHC.Builtin.Names
-import GHC.Data.FastString
 import GHC.Utils.Misc ( changeLast )
-import GHC.Core.TyCo.Rep -- Doesn't need special access, but this is easier to avoid
-                         -- import loops which show up if you import Type instead
-import {-# SOURCE #-} GHC.Core.Type ( mkTyConTy, mkTyConApp, mkTYPEapp, getLevity )
+import GHC.Utils.Panic ( assertPpr )
+import GHC.Utils.Outputable
 
+import GHC.Data.FastString
 import Data.Char
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-\subsection{Primitive type constructors}
+             Building blocks
 *                                                                      *
-************************************************************************
--}
+********************************************************************* -}
+
+mk_TYPE_app :: Type -> Type
+mk_TYPE_app rep = mkTyConApp tYPETyCon [rep]
+
+mk_CONSTRAINT_app :: Type -> Type
+mk_CONSTRAINT_app rep = mkTyConApp cONSTRAINTTyCon [rep]
+
+mkPrimTc :: FastString -> Unique -> TyCon -> Name
+mkPrimTc = mkGenPrimTc UserSyntax
+
+mkBuiltInPrimTc :: FastString -> Unique -> TyCon -> Name
+mkBuiltInPrimTc = mkGenPrimTc BuiltInSyntax
+
+mkGenPrimTc :: BuiltInSyntax -> FastString -> Unique -> TyCon -> Name
+mkGenPrimTc built_in_syntax occ key tycon
+  = mkWiredInName gHC_PRIM (mkTcOccFS occ)
+                  key
+                  (mkATyCon tycon)
+                  built_in_syntax
+
+-- | Create a primitive 'TyCon' with the given 'Name',
+-- arguments of kind 'Type` with the given 'Role's,
+-- and the given result kind representation.
+--
+-- Only use this in "GHC.Builtin.Types.Prim".
+pcPrimTyCon :: Name
+            -> [Role] -> RuntimeRepType -> TyCon
+pcPrimTyCon name roles res_rep
+  = mkPrimTyCon name binders result_kind roles
+  where
+    bndr_kis    = liftedTypeKind <$ roles
+    binders     = mkTemplateAnonTyConBinders bndr_kis
+    result_kind = mk_TYPE_app res_rep
+
+-- | Create a primitive nullary 'TyCon' with the given 'Name'
+-- and result kind representation.
+--
+-- Only use this in "GHC.Builtin.Types.Prim".
+pcPrimTyCon0 :: Name -> RuntimeRepType -> TyCon
+pcPrimTyCon0 name res_rep
+  = pcPrimTyCon name [] res_rep
+
+-- | Create a primitive 'TyCon' like 'pcPrimTyCon', except the last
+-- argument is levity-polymorphic, where the levity argument is
+-- implicit and comes before other arguments
+--
+-- Only use this in "GHC.Builtin.Types.Prim".
+pcPrimTyCon_LevPolyLastArg :: Name
+                           -> [Role] -- ^ roles of the arguments (must be non-empty),
+                                     -- not including the implicit argument of kind 'Levity',
+                                     -- which always has 'Nominal' role
+                           -> RuntimeRepType  -- ^ representation of the fully-applied type
+                           -> TyCon
+pcPrimTyCon_LevPolyLastArg name roles res_rep
+  = mkPrimTyCon name binders result_kind (Nominal : roles)
+    where
+      result_kind = mk_TYPE_app res_rep
+      lev_bndr = mkNamedTyConBinder Inferred levity1TyVar
+      binders  = lev_bndr : mkTemplateAnonTyConBinders anon_bndr_kis
+      lev_tv   = mkTyVarTy (binderVar lev_bndr)
+
+      -- [ Type, ..., Type, TYPE (BoxedRep l) ]
+      anon_bndr_kis = changeLast (liftedTypeKind <$ roles) $
+                      mk_TYPE_app $
+                      mkTyConApp boxedRepDataConTyCon [lev_tv]
+
+
+{- *********************************************************************
+*                                                                      *
+           Primitive type constructors
+*                                                                      *
+********************************************************************* -}
 
 primTyCons :: [TyCon]
 primTyCons = unexposedPrimTyCons ++ exposedPrimTyCons
@@ -160,6 +241,11 @@ unexposedPrimTyCons
   = [ eqPrimTyCon
     , eqReprPrimTyCon
     , eqPhantPrimTyCon
+
+    -- These are un-exposed for now
+    , ctArrowTyCon  -- (=>)
+    , ccArrowTyCon  -- (==>)
+    , tcArrowTyCon  -- (-=>)
     ]
 
 -- | Primitive 'TyCon's that are defined in, and exported from, GHC.Prim.
@@ -201,27 +287,13 @@ exposedPrimTyCons
     , stackSnapshotPrimTyCon
     , promptTagPrimTyCon
 
+    , fUNTyCon
     , tYPETyCon
-    , funTyCon
+    , cONSTRAINTTyCon
 
 #include "primop-vector-tycons.hs-incl"
     ]
 
-mkPrimTc :: FastString -> Unique -> TyCon -> Name
-mkPrimTc fs unique tycon
-  = mkWiredInName gHC_PRIM (mkTcOccFS fs)
-                  unique
-                  (mkATyCon tycon)        -- Relevant TyCon
-                  UserSyntax
-
-mkBuiltInPrimTc :: FastString -> Unique -> TyCon -> Name
-mkBuiltInPrimTc fs unique tycon
-  = mkWiredInName gHC_PRIM (mkTcOccFS fs)
-                  unique
-                  (mkATyCon tycon)        -- Relevant TyCon
-                  BuiltInSyntax
-
-
 charPrimTyConName, intPrimTyConName, int8PrimTyConName, int16PrimTyConName, int32PrimTyConName, int64PrimTyConName,
   wordPrimTyConName, word32PrimTyConName, word8PrimTyConName, word16PrimTyConName, word64PrimTyConName,
   addrPrimTyConName, floatPrimTyConName, doublePrimTyConName,
@@ -273,13 +345,13 @@ weakPrimTyConName             = mkPrimTc (fsLit "Weak#") weakPrimTyConKey weakPr
 threadIdPrimTyConName         = mkPrimTc (fsLit "ThreadId#") threadIdPrimTyConKey threadIdPrimTyCon
 promptTagPrimTyConName        = mkPrimTc (fsLit "PromptTag#") promptTagPrimTyConKey promptTagPrimTyCon
 
-{-
-************************************************************************
+{- *********************************************************************
 *                                                                      *
-\subsection{Support code}
+                Type variables
 *                                                                      *
-************************************************************************
+********************************************************************* -}
 
+{-
 alphaTyVars is a list of type variables for use in templates:
         ["a", "b", ..., "z", "t1", "t2", ... ]
 -}
@@ -366,13 +438,16 @@ mkTemplateKiTyVar kind mk_arg_kinds
 
 mkTemplateKindTyConBinders :: [Kind] -> [TyConBinder]
 -- Makes named, Specified binders
-mkTemplateKindTyConBinders kinds = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds]
+mkTemplateKindTyConBinders kinds
+  = [mkNamedTyConBinder Specified tv | tv <- mkTemplateKindVars kinds]
 
 mkTemplateAnonTyConBinders :: [Kind] -> [TyConBinder]
-mkTemplateAnonTyConBinders kinds = mkAnonTyConBinders VisArg (mkTemplateTyVars kinds)
+mkTemplateAnonTyConBinders kinds
+  = mkAnonTyConBinders (mkTemplateTyVars kinds)
 
 mkTemplateAnonTyConBindersFrom :: Int -> [Kind] -> [TyConBinder]
-mkTemplateAnonTyConBindersFrom n kinds = mkAnonTyConBinders VisArg (mkTemplateTyVarsFrom n kinds)
+mkTemplateAnonTyConBindersFrom n kinds
+  = mkAnonTyConBinders (mkTemplateTyVarsFrom n kinds)
 
 alphaTyVars :: [TyVar]
 alphaTyVars = mkTemplateTyVars $ repeat liftedTypeKind
@@ -383,6 +458,15 @@ alphaTyVar, betaTyVar, gammaTyVar, deltaTyVar :: TyVar
 alphaTyVarSpec, betaTyVarSpec, gammaTyVarSpec, deltaTyVarSpec :: TyVarBinder
 (alphaTyVarSpec:betaTyVarSpec:gammaTyVarSpec:deltaTyVarSpec:_) = mkTyVarBinders Specified alphaTyVars
 
+alphaConstraintTyVars :: [TyVar]
+alphaConstraintTyVars = mkTemplateTyVars $ repeat constraintKind
+
+alphaConstraintTyVar :: TyVar
+(alphaConstraintTyVar:_) = alphaConstraintTyVars
+
+alphaConstraintTy :: Type
+alphaConstraintTy = mkTyVarTy alphaConstraintTyVar
+
 alphaTys :: [Type]
 alphaTys = mkTyVarTys alphaTyVars
 alphaTy, betaTy, gammaTy, deltaTy :: Type
@@ -416,7 +500,9 @@ openAlphaTyVar, openBetaTyVar, openGammaTyVar :: TyVar
 -- beta  :: TYPE r2
 -- gamma :: TYPE r3
 [openAlphaTyVar,openBetaTyVar,openGammaTyVar]
-  = mkTemplateTyVars [mkTYPEapp runtimeRep1Ty, mkTYPEapp runtimeRep2Ty, mkTYPEapp runtimeRep3Ty]
+  = mkTemplateTyVars [ mk_TYPE_app runtimeRep1Ty
+                     , mk_TYPE_app runtimeRep2Ty
+                     , mk_TYPE_app runtimeRep3Ty]
 
 openAlphaTyVarSpec, openBetaTyVarSpec, openGammaTyVarSpec :: TyVarBinder
 openAlphaTyVarSpec = mkTyVarBinder Specified openAlphaTyVar
@@ -445,8 +531,8 @@ levity2Ty = mkTyVarTy levity2TyVar
 levPolyAlphaTyVar, levPolyBetaTyVar :: TyVar
 [levPolyAlphaTyVar, levPolyBetaTyVar] =
   mkTemplateTyVars
-    [mkTYPEapp (mkTyConApp boxedRepDataConTyCon [levity1Ty])
-    ,mkTYPEapp (mkTyConApp boxedRepDataConTyCon [levity2Ty])]
+    [ mk_TYPE_app (mkTyConApp boxedRepDataConTyCon [levity1Ty])
+    , mk_TYPE_app (mkTyConApp boxedRepDataConTyCon [levity2Ty])]
 -- alpha :: TYPE ('BoxedRep l)
 -- beta  :: TYPE ('BoxedRep k)
 
@@ -471,80 +557,257 @@ multiplicityTyVar1, multiplicityTyVar2  :: TyVar
 ************************************************************************
 -}
 
-funTyConName :: Name
-funTyConName = mkPrimTcName UserSyntax (fsLit "FUN") funTyConKey funTyCon
+{- Note [Function type constructors and FunTy]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+We have four distinct function type constructors, and a type synonym
+
+ FUN :: forall (m :: Multiplicity) ->
+        forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+        TYPE rep1 -> TYPE rep2 -> Type
+
+ (=>)  :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+          CONSTRAINT rep1 -> TYPE rep2 -> Type
+
+ (==>) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+          CONSTRAINT rep1 -> CONSTRAINT rep2 -> Constraint
+
+ (-=>) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+          TYPE rep1 -> CONSTRAINT rep2 -> Constraint
+
+ type (->) = FUN Many
+
+For efficiency, all four are always represented by
+  FunTy { ft_af :: FunTyFlag, ft_mult :: Mult
+        , ft_arg :: Type, ft_res :: Type }
+rather than by using a TyConApp.
+
+* The four TyCons FUN, (=>), (==>), (-=>) are all wired in.
+  But (->) is just a regular synonym, with no special treatment;
+  in particular it is not wired-in.
+
+* The ft_af :: FunTyFlag distinguishes the four cases.
+  See Note [FunTyFlag] in GHC.Types.Var.
+
+* The ft_af field is redundant: it can always be gleaned from
+  the kinds of ft_arg and ft_res.  See Note [FunTyFlag] in GHC.Types.Var.
+
+* The ft_mult :: Mult field gives the first argument for FUN
+  For the other three cases ft_mult is redundant; it is always Many.
+  Note that of the four type constructors, only `FUN` takes a Multiplicity.
+
+* Functions in GHC.Core.Type help to build and decompose `FunTy`.
+  * funTyConAppTy_maybe
+  * funTyFlagTyCon
+  * tyConAppFun_maybe
+  * splitFunTy_maybe
+  Use them!
+-}
+
+funTyFlagTyCon :: FunTyFlag -> TyCon
+-- `anonArgTyCon af` gets the TyCon that corresponds to the `FunTyFlag`
+-- But be careful: fUNTyCon has a different kind to the others!
+-- See Note [Function type constructors and FunTy]
+funTyFlagTyCon FTF_T_T = fUNTyCon
+funTyFlagTyCon FTF_T_C = tcArrowTyCon
+funTyFlagTyCon FTF_C_T = ctArrowTyCon
+funTyFlagTyCon FTF_C_C = ccArrowTyCon
+
+isArrowTyCon :: TyCon -> Bool
+-- We don't bother to look for plain (->), because this function
+-- should only be used after unwrapping synonyms
+isArrowTyCon tc
+  = assertPpr (not (isTypeSynonymTyCon tc)) (ppr tc)
+    getUnique tc `elem`
+    [fUNTyConKey, ctArrowTyConKey, ccArrowTyConKey, tcArrowTyConKey]
+
+fUNTyConName, ctArrowTyConName, ccArrowTyConName, tcArrowTyConName :: Name
+fUNTyConName     = mkPrimTc        (fsLit "FUN") fUNTyConKey       fUNTyCon
+ctArrowTyConName = mkBuiltInPrimTc (fsLit "=>")  ctArrowTyConKey ctArrowTyCon
+ccArrowTyConName = mkBuiltInPrimTc (fsLit "==>") ccArrowTyConKey ccArrowTyCon
+tcArrowTyConName = mkBuiltInPrimTc (fsLit "-=>") tcArrowTyConKey tcArrowTyCon
 
 -- | The @FUN@ type constructor.
 --
 -- @
 -- FUN :: forall (m :: Multiplicity) ->
 --        forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
---        TYPE rep1 -> TYPE rep2 -> *
+--        TYPE rep1 -> TYPE rep2 -> Type
 -- @
 --
 -- The runtime representations quantification is left inferred. This
 -- means they cannot be specified with @-XTypeApplications@.
 --
 -- This is a deliberate choice to allow future extensions to the
--- function arrow. To allow visible application a type synonym can be
--- defined:
---
--- @
--- type Arr :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
---             TYPE rep1 -> TYPE rep2 -> Type
--- type Arr = FUN 'Many
--- @
---
-funTyCon :: TyCon
-funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
+-- function arrow.
+fUNTyCon :: TyCon
+fUNTyCon = mkPrimTyCon fUNTyConName tc_bndrs liftedTypeKind tc_roles
   where
     -- See also unrestrictedFunTyCon
     tc_bndrs = [ mkNamedTyConBinder Required multiplicityTyVar1
                , mkNamedTyConBinder Inferred runtimeRep1TyVar
                , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
-               ++ mkTemplateAnonTyConBinders [ mkTYPEapp runtimeRep1Ty
-                                             , mkTYPEapp runtimeRep2Ty
-                                             ]
-    tc_rep_nm = mkPrelTyConRepName funTyConName
+               ++ mkTemplateAnonTyConBinders [ mk_TYPE_app runtimeRep1Ty
+                                             , mk_TYPE_app runtimeRep2Ty ]
+    tc_roles = [Nominal, Nominal, Nominal, Representational, Representational]
+
+-- (=>) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+--         CONSTRAINT rep1 -> TYPE rep2 -> Type
+ctArrowTyCon :: TyCon
+ctArrowTyCon = mkPrimTyCon ctArrowTyConName tc_bndrs liftedTypeKind tc_roles
+  where
+    -- See also unrestrictedFunTyCon
+    tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar
+               , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
+               ++ mkTemplateAnonTyConBinders [ mk_CONSTRAINT_app runtimeRep1Ty
+                                             , mk_TYPE_app       runtimeRep2Ty ]
+    tc_roles = [Nominal, Nominal, Representational, Representational]
+
+-- (==>) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+--          CONSTRAINT rep1 -> CONSTRAINT rep2 -> Constraint
+ccArrowTyCon :: TyCon
+ccArrowTyCon = mkPrimTyCon ccArrowTyConName tc_bndrs constraintKind tc_roles
+  where
+    -- See also unrestrictedFunTyCon
+    tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar
+               , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
+               ++ mkTemplateAnonTyConBinders [ mk_CONSTRAINT_app runtimeRep1Ty
+                                             , mk_CONSTRAINT_app runtimeRep2Ty ]
+    tc_roles = [Nominal, Nominal, Representational, Representational]
+
+-- (-=>) :: forall {rep1 :: RuntimeRep} {rep2 :: RuntimeRep}.
+--          TYPE rep1 -> CONSTRAINT rep2 -> Constraint
+tcArrowTyCon :: TyCon
+tcArrowTyCon = mkPrimTyCon tcArrowTyConName tc_bndrs constraintKind tc_roles
+  where
+    -- See also unrestrictedFunTyCon
+    tc_bndrs = [ mkNamedTyConBinder Inferred runtimeRep1TyVar
+               , mkNamedTyConBinder Inferred runtimeRep2TyVar ]
+               ++ mkTemplateAnonTyConBinders [ mk_TYPE_app       runtimeRep1Ty
+                                             , mk_CONSTRAINT_app runtimeRep2Ty ]
+    tc_roles = [Nominal, Nominal, Representational, Representational]
 
 {-
 ************************************************************************
 *                                                                      *
-                Kinds
+                Type and Constraint
 *                                                                      *
 ************************************************************************
 
-Note [TYPE and RuntimeRep]
+Note [TYPE and CONSTRAINT]  aka Note [Type vs Constraint]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~
-All types that classify values have a kind of the form (TYPE rr), where
+GHC distinguishes Type from Constraint throughout the compiler.
+See GHC Proposal #518, and tickets #21623 and #11715.
+
+All types that classify values have a kind of the form
+  (TYPE rr) or (CONSTRAINT rr)
+where the `RuntimeRep` parameter, rr, tells us how the value is represented
+at runtime.  TYPE and CONSTRAINT are primitive type constructors.
+
+See Note [RuntimeRep polymorphism] about the `rr` parameter.
+
+There are a bunch of type synonyms and data types defined in the
+library ghc-prim:GHC.Types.  All of them are also wired in to GHC, in
+GHC.Builtin.Types
+
+  type Constraint   = CONSTRAINT LiftedRep  :: Type
+
+  type Type         = TYPE LiftedRep   :: Type
+  type UnliftedType = TYPE UnliftedRep :: Type
+
+  type LiftedRep    = BoxedRep Lifted   :: RuntimeRep
+  type UnliftedRep  = BoxedRep Unlifted :: RuntimeRep
 
-    data RuntimeRep     -- Defined in ghc-prim:GHC.Types
+  data RuntimeRep     -- Defined in ghc-prim:GHC.Types
       = BoxedRep Levity
       | IntRep
       | FloatRep
       .. etc ..
 
-    data Levity = Lifted | Unlifted
+  data Levity = Lifted | Unlifted
 
-    rr :: RuntimeRep
-
-    TYPE :: RuntimeRep -> TYPE 'LiftedRep  -- Built in
+We abbreviate '*' specially (with -XStarIsType), as if we had this:
+    type * = Type
 
 So for example:
-    Int        :: TYPE ('BoxedRep 'Lifted)
-    Array# Int :: TYPE ('BoxedRep 'Unlifted)
-    Int#       :: TYPE 'IntRep
-    Float#     :: TYPE 'FloatRep
-    Maybe      :: TYPE ('BoxedRep 'Lifted) -> TYPE ('BoxedRep 'Lifted)
+    Int        :: TYPE (BoxedRep Lifted)
+    Array# Int :: TYPE (BoxedRep Unlifted)
+    Int#       :: TYPE IntRep
+    Float#     :: TYPE FloatRep
+    Maybe      :: TYPE (BoxedRep Lifted) -> TYPE (BoxedRep Lifted)
     (# , #)    :: TYPE r1 -> TYPE r2 -> TYPE (TupleRep [r1, r2])
 
-We abbreviate '*' specially:
-    type LiftedRep = 'BoxedRep 'Lifted
-    type * = TYPE LiftedRep
+    Eq Int       :: CONSTRAINT (BoxedRep Lifted)
+    IP "foo" Int :: CONSTRAINT (BoxedRep Lifted)
+    a ~ b        :: CONSTRAINT (BoxedRep Lifted)
+    a ~# b       :: CONSTRAINT (TupleRep [])
+
+Constraints are mostly lifted, but unlifted ones are useful too.
+Specifically  (a ~# b) :: CONSTRAINT (TupleRep [])
+
+Wrinkles
+
+(W1) Type and Constraint are considered distinct throughout GHC. But they
+     are not /apart/: see Note [Type and Constraint are not apart]
+
+(W2) We need two absent-error Ids, aBSENT_ERROR_ID for types of kind Type, and
+     aBSENT_CONSTRAINT_ERROR_ID for vaues of kind Constraint.  Ditto noInlineId
+     vs noInlieConstraintId in GHC.Types.Id.Make; see Note [inlineId magic].
+
+(W3) We need a TypeOrConstraint flag in LitRubbish.
+
+Note [Type and Constraint are not apart]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Type and Constraint are not equal (eqType) but they are not /apart/
+either. Reason (c.f. #7451):
+
+* We want to allow newtype classes, where
+    class C a where { op :: a -> a }
+
+* The axiom for such a class will look like
+    axiom axC a :: (C a :: Constraint) ~# (a->a :: Type)
+
+* This axiom connects a type of kind Type with one of kind Constraint
+  That is dangerous: kindCo (axC Int) :: Type ~N Constraint
+  In general, having a "contradictory proof" like (Int ~N Bool) would be
+  Very Bad; but it's fine provided they are not Apart.
+
+So we ensure that Type and Constraint are not apart; or, more
+precisely, that TYPE and CONSTRAINT are not apart.  This
+non-apart-ness check is implemented in GHC.Core.Unify.unify_ty: look
+for `maybeApart MARTypeVsConstraint`.
+
+Note that, as before, nothing prevents writing instances like:
 
-The 'rr' parameter tells us how the value is represented at runtime.
+  instance C (Proxy @Type a) where ...
 
-Generally speaking, you can't be polymorphic in 'rr'.  E.g
+In particular, TYPE and CONSTRAINT (and the synonyms Type, Constraint
+etc) are all allowed in instance heads. It's just that TYPE is not
+apart from CONSTRAINT, which means that the above instance would
+irretrievably overlap with:
+
+  instance C (Proxy @Constraint a) where ...
+
+Wrinkles
+
+(W1) In GHC.Core.RoughMap.roughMapTyConName we are careful to map
+     TYPE and CONSTRAINT to the same rough-map key.
+     **ToDo**: explain why
+
+(W2) We must extend this treatment to the different arrow types (see
+     Note [Function type constructors and FunTy]): if we have
+     FunCo (axC Int) <Int> :: (C Int => Int) ~ ((Int -> Int) -> Int), then
+     we could extract an equality between (=>) and (->). We thus must ensure
+     that (=>) and (->) (among the other arrow combinations) are not Apart.
+     See the FunTy/FunTy case in GHC.Core.Unify.unify_ty
+
+(W3) Are (TYPE IntRep) and (CONSTRAINT WordRep) apart?  In fact yes, they are.
+     But it's easier to report "maybeApart", rather than recurse into the
+     arguments (whose kinds may be utterly different) to look for apartness
+     inside them  Again this is in GHC.Core.Unify.unify_ty.
+
+Note [RuntimeRep polymorphism]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+Generally speaking, you can't be polymorphic in `RuntimeRep`.  E.g
    f :: forall (rr:RuntimeRep) (a:TYPE rr). a -> [a]
    f = /\(rr:RuntimeRep) (a:rr) \(a:rr). ...
 This is no good: we could not generate code for 'f', because the
@@ -569,85 +832,40 @@ generator never has to manipulate a value of type 'a :: TYPE rr'.
      (#,#) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
                      (a :: TYPE r1) (b :: TYPE r2).
                      a -> b -> TYPE ('TupleRep '[r1, r2])
-
 -}
 
+----------------------
 tYPETyCon :: TyCon
-tYPETyConName :: Name
-
 tYPETyCon = mkPrimTyCon tYPETyConName
                         (mkTemplateAnonTyConBinders [runtimeRepTy])
                         liftedTypeKind
                         [Nominal]
 
---------------------------
--- ... and now their names
+tYPETyConName :: Name
+tYPETyConName = mkPrimTc (fsLit "TYPE") tYPETyConKey tYPETyCon
 
--- If you edit these, you may need to update the GHC formalism
--- See Note [GHC Formalism] in GHC.Core.Lint
-tYPETyConName             = mkPrimTcName UserSyntax (fsLit "TYPE") tYPETyConKey tYPETyCon
+tYPEKind :: Type
+tYPEKind = mkTyConTy tYPETyCon
 
-mkPrimTcName :: BuiltInSyntax -> FastString -> Unique -> TyCon -> Name
-mkPrimTcName built_in_syntax occ key tycon
-  = mkWiredInName gHC_PRIM (mkTcOccFS occ) key (mkATyCon tycon) built_in_syntax
+----------------------
+cONSTRAINTTyCon :: TyCon
+cONSTRAINTTyCon = mkPrimTyCon cONSTRAINTTyConName
+                              (mkTemplateAnonTyConBinders [runtimeRepTy])
+                              liftedTypeKind
+                              [Nominal]
 
------------------------------
+cONSTRAINTTyConName :: Name
+cONSTRAINTTyConName = mkPrimTc (fsLit "CONSTRAINT") cONSTRAINTTyConKey cONSTRAINTTyCon
 
--- Given a Multiplicity, applies FUN to it.
-functionWithMultiplicity :: Type -> Type
-functionWithMultiplicity mul = TyConApp funTyCon [mul]
+cONSTRAINTKind :: Type
+cONSTRAINTKind = mkTyConTy cONSTRAINTTyCon
 
-{-
-************************************************************************
+
+{- *********************************************************************
 *                                                                      *
-   Basic primitive types (@Char#@, @Int#@, etc.)
+       Basic primitive types (Char#, Int#, etc.)
 *                                                                      *
-************************************************************************
--}
-
--- | Create a primitive 'TyCon' with the given 'Name',
--- arguments of kind 'Type` with the given 'Role's,
--- and the given result kind representation.
---
--- Only use this in "GHC.Builtin.Types.Prim".
-pcPrimTyCon :: Name
-            -> [Role] -> RuntimeRepType -> TyCon
-pcPrimTyCon name roles res_rep
-  = mkPrimTyCon name binders result_kind roles
-  where
-    bndr_kis    = liftedTypeKind <$ roles
-    binders     = mkTemplateAnonTyConBinders bndr_kis
-    result_kind = mkTYPEapp res_rep
-
--- | Create a primitive nullary 'TyCon' with the given 'Name'
--- and result kind representation.
---
--- Only use this in "GHC.Builtin.Types.Prim".
-pcPrimTyCon0 :: Name -> RuntimeRepType -> TyCon
-pcPrimTyCon0 name res_rep
-  = pcPrimTyCon name [] res_rep
-
--- | Create a primitive 'TyCon' like 'pcPrimTyCon', except the last
--- argument is levity-polymorphic.
---
--- Only use this in "GHC.Builtin.Types.Prim".
-pcPrimTyCon_LevPolyLastArg :: Name
-                           -> [Role] -- ^ roles of the arguments (must be non-empty),
-                                     -- not including the implicit argument of kind 'Levity',
-                                     -- which always has 'Nominal' role
-                           -> RuntimeRepType  -- ^ representation of the fully-applied type
-                           -> TyCon
-pcPrimTyCon_LevPolyLastArg name roles res_rep
-  = mkPrimTyCon name binders result_kind (Nominal : roles)
-    where
-      result_kind = mkTYPEapp res_rep
-      lev_bndr = mkNamedTyConBinder Inferred levity1TyVar
-      binders  = lev_bndr : mkTemplateAnonTyConBinders anon_bndr_kis
-      lev_tv   = mkTyVarTy (binderVar lev_bndr)
-
-      -- [ Type, ..., Type, TYPE (BoxedRep l) ]
-      anon_bndr_kis = changeLast (liftedTypeKind <$ roles)
-                        (mkTYPEapp $ mkTyConApp boxedRepDataConTyCon [lev_tv])
+********************************************************************* -}
 
 charPrimTy :: Type
 charPrimTy      = mkTyConTy charPrimTyCon
@@ -818,6 +1036,8 @@ It is an almost-ordinary class defined as if by
  * In addition (~) is magical syntax, as ~ is a reserved symbol.
    It cannot be exported or imported.
 
+ * The data constructor of the class is "Eq#", not ":C~"
+
 Within GHC, ~ is called eqTyCon, and it is defined in GHC.Builtin.Types.
 
 Historical note: prior to July 18 (~) was defined as a
@@ -944,9 +1164,9 @@ eqPrimTyCon :: TyCon  -- The representation type for equality predicates
                       -- See Note [The equality types story]
 eqPrimTyCon  = mkPrimTyCon eqPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
+    -- Kind :: forall k1 k2. k1 -> k2 -> CONSTRAINT ZeroBitRep
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
-    res_kind = unboxedTupleKind []
+    res_kind = TyConApp cONSTRAINTTyCon [zeroBitRepTy]
     roles    = [Nominal, Nominal, Nominal, Nominal]
 
 -- like eqPrimTyCon, but the type for *Representational* coercions
@@ -955,9 +1175,9 @@ eqPrimTyCon  = mkPrimTyCon eqPrimTyConName binders res_kind roles
 eqReprPrimTyCon :: TyCon   -- See Note [The equality types story]
 eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
+    -- Kind :: forall k1 k2. k1 -> k2 -> CONSTRAINT ZeroBitRep
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
-    res_kind = unboxedTupleKind []
+    res_kind = TyConApp cONSTRAINTTyCon [zeroBitRepTy]
     roles    = [Nominal, Nominal, Representational, Representational]
 
 -- like eqPrimTyCon, but the type for *Phantom* coercions.
@@ -966,9 +1186,9 @@ eqReprPrimTyCon = mkPrimTyCon eqReprPrimTyConName binders res_kind roles
 eqPhantPrimTyCon :: TyCon
 eqPhantPrimTyCon = mkPrimTyCon eqPhantPrimTyConName binders res_kind roles
   where
-    -- Kind :: forall k1 k2. k1 -> k2 -> TYPE (TupleRep '[])
+    -- Kind :: forall k1 k2. k1 -> k2 -> CONSTRAINT ZeroBitRep
     binders  = mkTemplateTyConBinders [liftedTypeKind, liftedTypeKind] id
-    res_kind = unboxedTupleKind []
+    res_kind = TyConApp cONSTRAINTTyCon [zeroBitRepTy]
     roles    = [Nominal, Nominal, Phantom, Phantom]
 
 -- | Given a Role, what TyCon is the type of equality predicates at that role?

compiler/GHC/Builtin/Types/Prim.hs-boot

-module GHC.Builtin.Types.Prim where
-
-import GHC.Core.TyCon
-
-tYPETyCon :: TyCon

compiler/GHC/Builtin/Uniques.hs

@@ -13,8 +13,8 @@ module GHC.Builtin.Uniques
 
       -- * Getting the 'Unique's of 'Name's
       -- ** Anonymous sums
-    , mkSumTyConUnique
-    , mkSumDataConUnique
+    , mkSumTyConUnique, mkSumDataConUnique
+
       -- ** Tuples
       -- *** Vanilla
     , mkTupleTyConUnique
@@ -45,6 +45,9 @@ module GHC.Builtin.Uniques
 
     , initExitJoinUnique
 
+      -- Boxing data types
+    , mkBoxingTyConUnique, boxingDataConUnique
+
     ) where
 
 import GHC.Prelude
@@ -297,6 +300,7 @@ Allocation of unique supply characters:
         other a-z: lower case chars for unique supplies.  Used so far:
 
         a       TypeChecking?
+        b       Boxing tycons & datacons
         c       StgToCmm/Renamer
         d       desugarer
         f       AbsC flattener
@@ -310,6 +314,27 @@ Allocation of unique supply characters:
         u       Cmm pipeline
         y       GHCi bytecode generator
         z       anonymous sums
+
+Note [Related uniques for wired-in things]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+* All wired in tycons actually use *two* uniques:
+  * u: the TyCon itself
+  * u+1: the TyConRepName of the TyCon (for use with TypeRep)
+  The "+1" is implemented in tyConRepNameUnique.
+  If this ever changes, make sure to also change the treatment for boxing tycons.
+
+* All wired in datacons use *three* uniques:
+  * u: the DataCon itself
+  * u+1: its worker Id
+  * u+2: the TyConRepName of the promoted TyCon
+  No wired-in datacons have wrappers.
+  The "+1" is implemented in dataConWorkerUnique and the "+2" is in dataConTyRepNameUnique.
+  If this ever changes, make sure to also change the treatment for boxing tycons.
+
+* Because boxing tycons (see Note [Boxing constructors] in GHC.Builtin.Types)
+  come with both a tycon and a datacon, each one takes up five slots, combining
+  the two cases above. Getting from the tycon to the datacon (by adding 2)
+  is implemented in boxingDataConUnique.
 -}
 
 mkAlphaTyVarUnique     :: Int -> Unique
@@ -351,29 +376,48 @@ mkTcOccUnique   fs = mkUnique 'c' (uniqueOfFS fs)
 initExitJoinUnique :: Unique
 initExitJoinUnique = mkUnique 's' 0
 
-
 --------------------------------------------------
 -- Wired-in type constructor keys occupy *two* slots:
---    * u: the TyCon itself
---    * u+1: the TyConRepName of the TyCon
+-- See Note [Related uniques for wired-in things]
 
 mkPreludeTyConUnique   :: Int -> Unique
-mkPreludeTyConUnique i                = mkUnique '3' (2*i)
+mkPreludeTyConUnique i = mkUnique '3' (2*i)
 
 tyConRepNameUnique :: Unique -> Unique
 tyConRepNameUnique  u = incrUnique u
 
 --------------------------------------------------
 -- Wired-in data constructor keys occupy *three* slots:
---    * u: the DataCon itself
---    * u+1: its worker Id
---    * u+2: the TyConRepName of the promoted TyCon
--- Prelude data constructors are too simple to need wrappers.
+-- See Note [Related uniques for wired-in things]
 
 mkPreludeDataConUnique :: Int -> Unique
-mkPreludeDataConUnique i              = mkUnique '6' (3*i)    -- Must be alphabetic
+mkPreludeDataConUnique i = mkUnique '6' (3*i)    -- Must be alphabetic
 
---------------------------------------------------
 dataConTyRepNameUnique, dataConWorkerUnique :: Unique -> Unique
 dataConWorkerUnique  u = incrUnique u
 dataConTyRepNameUnique u = stepUnique u 2
+
+--------------------------------------------------
+-- The data constructors of RuntimeRep occupy *five* slots:
+-- See Note [Related uniques for wired-in things]
+--
+--    Example: WordRep
+--
+-- * u: the TyCon of the boxing data type WordBox
+-- * u+1: the TyConRepName of the boxing data type
+-- * u+2: the DataCon for MkWordBox
+-- * u+3: the worker id for MkWordBox
+-- * u+4: the TyConRepName of the promoted TyCon 'MkWordBox
+--
+-- Note carefully that
+-- * u,u+1 are in sync with the conventions for
+--          wired-in type constructors, above
+-- * u+2,u+3,u+4 are in sync with the conventions for
+--               wired-in data constructors, above
+-- A little delicate!
+
+mkBoxingTyConUnique :: Int -> Unique
+mkBoxingTyConUnique i = mkUnique 'b' (5*i)
+
+boxingDataConUnique :: Unique -> Unique
+boxingDataConUnique u = stepUnique u 2

compiler/GHC/Core/Coercion.hs

@@ -13,7 +13,9 @@
 --
 module GHC.Core.Coercion (
         -- * Main data type
-        Coercion, CoercionN, CoercionR, CoercionP, MCoercion(..), MCoercionN, MCoercionR,
+        Coercion, CoercionN, CoercionR, CoercionP,
+        MCoercion(..), MCoercionN, MCoercionR,
+        CoSel(..), FunSel(..),
         UnivCoProvenance, CoercionHole(..),
         coHoleCoVar, setCoHoleCoVar,
         LeftOrRight(..),
@@ -35,8 +37,10 @@ module GHC.Core.Coercion (
         mkAxInstLHS, mkUnbranchedAxInstLHS,
         mkPiCo, mkPiCos, mkCoCast,
         mkSymCo, mkTransCo,
-        mkNthCo, mkNthCoFunCo, nthCoRole, mkLRCo,
-        mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo, mkFunCo, mkFunResCo,
+        mkSelCo, getNthFun, getNthFromType, mkLRCo,
+        mkInstCo, mkAppCo, mkAppCos, mkTyConAppCo,
+        mkFunCo1, mkFunCo2, mkFunCoNoFTF, mkFunResCo,
+        mkNakedFunCo1, mkNakedFunCo2,
         mkForAllCo, mkForAllCos, mkHomoForAllCos,
         mkPhantomCo,
         mkHoleCo, mkUnivCo, mkSubCo,
@@ -56,14 +60,13 @@ module GHC.Core.Coercion (
         topNormaliseNewType_maybe, topNormaliseTypeX,
 
         decomposeCo, decomposeFunCo, decomposePiCos, getCoVar_maybe,
-        splitTyConAppCo_maybe,
         splitAppCo_maybe,
         splitFunCo_maybe,
         splitForAllCo_maybe,
         splitForAllCo_ty_maybe, splitForAllCo_co_maybe,
 
-        nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
-
+        tyConRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
+        funRole,
         pickLR,
 
         isGReflCo, isReflCo, isReflCo_maybe, isGReflCo_maybe, isReflexiveCo, isReflexiveCo_maybe,
@@ -118,7 +121,7 @@ module GHC.Core.Coercion (
         -- * Other
         promoteCoercion, buildCoercion,
 
-        multToCo,
+        multToCo, mkRuntimeRepCo,
 
         hasCoercionHoleTy, hasCoercionHoleCo, hasThisCoercionHoleTy,
 
@@ -135,11 +138,11 @@ import GHC.Core.TyCo.FVs
 import GHC.Core.TyCo.Ppr
 import GHC.Core.TyCo.Subst
 import GHC.Core.TyCo.Tidy
+import GHC.Core.TyCo.Compare( eqType, eqTypeX )
 import GHC.Core.Type
 import GHC.Core.TyCon
 import GHC.Core.TyCon.RecWalk
 import GHC.Core.Coercion.Axiom
-import {-# SOURCE #-} GHC.Core.Utils ( mkFunctionType )
 import GHC.Types.Var
 import GHC.Types.Var.Env
 import GHC.Types.Var.Set
@@ -245,7 +248,7 @@ ppr_co_ax_branch :: (TidyEnv -> Type -> SDoc)
                  -> TyCon -> CoAxBranch -> SDoc
 ppr_co_ax_branch ppr_rhs fam_tc branch
   = foldr1 (flip hangNotEmpty 2)
-    [ pprUserForAll (mkTyCoVarBinders Inferred bndrs')
+    [ pprUserForAll (mkForAllTyBinders Inferred bndrs')
          -- See Note [Printing foralls in type family instances] in GHC.Iface.Type
     , pp_lhs <+> ppr_rhs tidy_env ee_rhs
     , text "-- Defined" <+> pp_loc ]
@@ -359,9 +362,9 @@ mkPiMCos :: [Var] -> MCoercion -> MCoercion
 mkPiMCos _ MRefl = MRefl
 mkPiMCos vs (MCo co) = MCo (mkPiCos Representational vs co)
 
-mkFunResMCo :: Scaled Type -> MCoercionR -> MCoercionR
+mkFunResMCo :: Id -> MCoercionR -> MCoercionR
 mkFunResMCo _      MRefl    = MRefl
-mkFunResMCo arg_ty (MCo co) = MCo (mkFunResCo Representational arg_ty co)
+mkFunResMCo arg_id (MCo co) = MCo (mkFunResCo Representational arg_id co)
 
 mkGReflLeftMCo :: Role -> Type -> MCoercionN -> Coercion
 mkGReflLeftMCo r ty MRefl    = mkReflCo r ty
@@ -386,22 +389,8 @@ isReflMCo _     = False
         Destructing coercions
 %*                                                                      *
 %************************************************************************
-
-Note [Function coercions]
-~~~~~~~~~~~~~~~~~~~~~~~~~
-Remember that
-  (->) :: forall {r1} {r2}. TYPE r1 -> TYPE r2 -> TYPE LiftedRep
-whose `RuntimeRep' arguments are intentionally marked inferred to
-avoid type application.
-
-Hence
-  FunCo r mult co1 co2 :: (s1->t1) ~r (s2->t2)
-is short for
-  TyConAppCo (->) mult co_rep1 co_rep2 co1 co2
-where co_rep1, co_rep2 are the coercions on the representations.
 -}
 
-
 -- | This breaks a 'Coercion' with type @T A B C ~ T D E F@ into
 -- a list of 'Coercion's of kinds @A ~ D@, @B ~ E@ and @E ~ F@. Hence:
 --
@@ -412,22 +401,25 @@ decomposeCo :: Arity -> Coercion
                        -- entries as the Arity provided
             -> [Coercion]
 decomposeCo arity co rs
-  = [mkNthCo r n co | (n,r) <- [0..(arity-1)] `zip` rs ]
-           -- Remember, Nth is zero-indexed
+  = [mkSelCo (SelTyCon n r) co | (n,r) <- [0..(arity-1)] `zip` rs ]
+     -- Remember, SelTyCon is zero-indexed
 
 decomposeFunCo :: HasDebugCallStack
-               => Role      -- Role of the input coercion
-               -> Coercion  -- Input coercion
+               => Coercion  -- Input coercion
                -> (CoercionN, Coercion, Coercion)
--- Expects co :: (s1 -> t1) ~ (s2 -> t2)
--- Returns (co1 :: s1~s2, co2 :: t1~t2)
--- See Note [Function coercions] for the "3" and "4"
-
-decomposeFunCo _ (FunCo _ w co1 co2) = (w, co1, co2)
-   -- Short-circuits the calls to mkNthCo
-
-decomposeFunCo r co = assertPpr all_ok (ppr co)
-                      (mkNthCo Nominal 0 co, mkNthCo r 3 co, mkNthCo r 4 co)
+-- Expects co :: (s1 %m1-> t1) ~ (s2 %m2-> t2)
+-- Returns (cow :: m1 ~N m2, co1 :: s1~s2, co2 :: t1~t2)
+-- actually cow will be a Phantom coercion if the input is a Phantom coercion
+
+decomposeFunCo (FunCo { fco_mult = w, fco_arg = co1, fco_res = co2 })
+  = (w, co1, co2)
+   -- Short-circuits the calls to mkSelCo
+
+decomposeFunCo co
+  = assertPpr all_ok (ppr co) $
+    ( mkSelCo (SelFun SelMult) co
+    , mkSelCo (SelFun SelArg) co
+    , mkSelCo (SelFun SelRes) co )
   where
     Pair s1t1 s2t2 = coercionKind co
     all_ok = isFunTy s1t1 && isFunTy s2t2
@@ -488,24 +480,25 @@ decomposePiCos orig_co (Pair orig_k1 orig_k2) orig_args
         --          ty :: s2
         -- need arg_co :: s2 ~ s1
         --      res_co :: t1[ty |> arg_co / a] ~ t2[ty / b]
-      = let arg_co  = mkNthCo Nominal 0 (mkSymCo co)
+      = let arg_co  = mkSelCo SelForAll (mkSymCo co)
             res_co  = mkInstCo co (mkGReflLeftCo Nominal ty arg_co)
             subst1' = extendTCvSubst subst1 a (ty `CastTy` arg_co)
             subst2' = extendTCvSubst subst2 b ty
         in
         go (arg_co : acc_arg_cos) (subst1', t1) res_co (subst2', t2) tys
 
-      | Just (_w1, _s1, t1) <- splitFunTy_maybe k1
-      , Just (_w1, _s2, t2) <- splitFunTy_maybe k2
+      | Just (af1, _w1, _s1, t1) <- splitFunTy_maybe k1
+      , Just (af2, _w1, _s2, t2) <- splitFunTy_maybe k2
+      , af1 == af2  -- Same sort of arrow
         -- know     co :: (s1 -> t1) ~ (s2 -> t2)
         --    function :: s1 -> t1
         --          ty :: s2
         -- need arg_co :: s2 ~ s1
         --      res_co :: t1 ~ t2
-      = let (_, sym_arg_co, res_co) = decomposeFunCo Nominal co
-            -- It should be fine to ignore the multiplicity bit of the coercion
-            -- for a Nominal coercion.
-            arg_co               = mkSymCo sym_arg_co
+      = let (_, sym_arg_co, res_co) = decomposeFunCo co
+            -- It should be fine to ignore the multiplicity bit
+            -- of the coercion for a Nominal coercion.
+            arg_co = mkSymCo sym_arg_co
         in
         go (arg_co : acc_arg_cos) (subst1,t1) res_co (subst2,t2) tys
 
@@ -526,19 +519,6 @@ getCoVar_maybe :: Coercion -> Maybe CoVar
 getCoVar_maybe (CoVarCo cv) = Just cv
 getCoVar_maybe _            = Nothing
 
--- | Attempts to tease a coercion apart into a type constructor and the application
--- of a number of coercion arguments to that constructor
-splitTyConAppCo_maybe :: Coercion -> Maybe (TyCon, [Coercion])
-splitTyConAppCo_maybe co
-  | Just (ty, r) <- isReflCo_maybe co
-  = do { (tc, tys) <- splitTyConApp_maybe ty
-       ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
-       ; return (tc, args) }
-splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
-splitTyConAppCo_maybe (FunCo _ w arg res)     = Just (funTyCon, cos)
-  where cos = [w, mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
-splitTyConAppCo_maybe _                     = Nothing
-
 multToCo :: Mult -> Coercion
 multToCo r = mkNomReflCo r
 
@@ -551,10 +531,10 @@ splitAppCo_maybe (TyConAppCo r tc args)
   , Just (args', arg') <- snocView args
   = Just ( mkTyConAppCo r tc args', arg' )
 
-  | not (mustBeSaturated tc)
+  | not (tyConMustBeSaturated tc)
     -- Never create unsaturated type family apps!
   , Just (args', arg') <- snocView args
-  , Just arg'' <- setNominalRole_maybe (nthRole r tc (length args')) arg'
+  , Just arg'' <- setNominalRole_maybe (tyConRole r tc (length args')) arg'
   = Just ( mkTyConAppCo r tc args', arg'' )
        -- Use mkTyConAppCo to preserve the invariant
        --  that identity coercions are always represented by Refl
@@ -567,7 +547,7 @@ splitAppCo_maybe _ = Nothing
 
 -- Only used in specialise/Rules
 splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
-splitFunCo_maybe (FunCo _ _ arg res) = Just (arg, res)
+splitFunCo_maybe (FunCo { fco_arg = arg, fco_res = res }) = Just (arg, res)
 splitFunCo_maybe _ = Nothing
 
 splitForAllCo_maybe :: Coercion -> Maybe (TyCoVar, Coercion, Coercion)
@@ -628,13 +608,13 @@ eqTyConRole tc
   = pprPanic "eqTyConRole: unknown tycon" (ppr tc)
 
 -- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
+--   (or CONSTRAINT instead of TYPE)
 -- produce a coercion @rep_co :: r1 ~ r2@.
 mkRuntimeRepCo :: HasDebugCallStack => Coercion -> Coercion
 mkRuntimeRepCo co
-  = mkNthCo Nominal 0 kind_co
+  = mkSelCo (SelTyCon 0 Nominal) kind_co
   where
     kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
-                           -- (up to silliness with Constraint)
 
 isReflCoVar_maybe :: Var -> Maybe Coercion
 -- If cv :: t~t then isReflCoVar_maybe cv = Just (Refl t)
@@ -707,7 +687,6 @@ of Coercion, and they perform very basic optimizations.
 
 Note [Role twiddling functions]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 There are a plethora of functions for twiddling roles:
 
 mkSubCo: Requires a nominal input coercion and always produces a
@@ -773,14 +752,10 @@ mkNomReflCo = Refl
 -- caller's responsibility to get the roles correct on argument coercions.
 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkTyConAppCo r tc cos
-  | [w, _rep1, _rep2, co1, co2] <- cos   -- See Note [Function coercions]
-  , isFunTyCon tc
-  = -- (a :: TYPE ra) -> (b :: TYPE rb)  ~  (c :: TYPE rc) -> (d :: TYPE rd)
-    -- rep1 :: ra  ~  rc        rep2 :: rb  ~  rd
-    -- co1  :: a   ~  c         co2  :: b   ~  d
-    mkFunCo r w co1 co2
-
-               -- Expand type synonyms
+  | Just co <- tyConAppFunCo_maybe r tc cos
+  = co
+
+  -- Expand type synonyms
   | ExpandsSyn tv_co_prs rhs_ty leftover_cos <- expandSynTyCon_maybe tc cos
   = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
 
@@ -790,17 +765,85 @@ mkTyConAppCo r tc cos
 
   | otherwise = TyConAppCo r tc cos
 
+mkFunCoNoFTF :: HasDebugCallStack => Role -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This version of mkFunCo takes no FunTyFlags; it works them out
+mkFunCoNoFTF r w arg_co res_co
+  = mkFunCo2 r afl afr w arg_co res_co
+  where
+    afl = chooseFunTyFlag argl_ty resl_ty
+    afr = chooseFunTyFlag argr_ty resr_ty
+    Pair argl_ty argr_ty = coercionKind arg_co
+    Pair resl_ty resr_ty = coercionKind res_co
+
 -- | Build a function 'Coercion' from two other 'Coercion's. That is,
 -- given @co1 :: a ~ b@ and @co2 :: x ~ y@ produce @co :: (a -> x) ~ (b -> y)@
 -- or @(a => x) ~ (b => y)@, depending on the kind of @a@/@b@.
-mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
-mkFunCo r w co1 co2
-    -- See Note [Refl invariant]
-  | Just (ty1, _) <- isReflCo_maybe co1
-  , Just (ty2, _) <- isReflCo_maybe co2
-  , Just (w, _) <- isReflCo_maybe w
-  = mkReflCo r (mkFunctionType w ty1 ty2)
-  | otherwise = FunCo r w co1 co2
+-- This (most common) version takes a single FunTyFlag, which is used
+--   for both fco_afl and ftf_afr of the FunCo
+mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo1 r af w arg_co res_co
+  = mkFunCo2 r af af w arg_co res_co
+
+mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This version of mkFunCo1 does not check FunCo invariants (checkFunCo)
+-- It is called during typechecking on un-zonked types;
+-- in particular there may be un-zonked coercion variables.
+mkNakedFunCo1 r af w arg_co res_co
+  = mkNakedFunCo2 r af af w arg_co res_co
+
+mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag
+                              -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This is the smart constructor for FunCo; it checks invariants
+mkFunCo2 r afl afr w arg_co res_co
+  = assertPprMaybe (checkFunCo r afl afr w arg_co res_co) $
+    mkNakedFunCo2 r afl afr w arg_co res_co
+
+mkNakedFunCo2 :: Role -> FunTyFlag -> FunTyFlag
+              -> CoercionN -> Coercion -> Coercion -> Coercion
+-- This is the smart constructor for FunCo
+-- "Naked"; it does not check invariants
+mkNakedFunCo2 r afl afr w arg_co res_co
+  | Just (ty1, _) <- isReflCo_maybe arg_co
+  , Just (ty2, _) <- isReflCo_maybe res_co
+  , Just (w, _)   <- isReflCo_maybe w
+  = mkReflCo r (mkFunTy afl w ty1 ty2)  -- See Note [Refl invariant]
+
+  | otherwise
+  = FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
+          , fco_mult = w, fco_arg = arg_co, fco_res = res_co }
+
+
+checkFunCo :: Role -> FunTyFlag -> FunTyFlag
+           -> CoercionN -> Coercion -> Coercion
+           -> Maybe SDoc
+-- Checks well-formed-ness for FunCo
+-- Used only in assertions and Lint
+{-# NOINLINE checkFunCo #-}
+checkFunCo _r afl afr _w arg_co res_co
+  | not (ok argl_ty && ok argr_ty && ok resl_ty && ok resr_ty)
+  = Just (hang (text "Bad arg or res types") 2 pp_inputs)
+
+  | afl == computed_afl
+  , afr == computed_afr
+  = Nothing
+  | otherwise
+  = Just (vcat [ text "afl (provided,computed):" <+> ppr afl <+> ppr computed_afl
+               , text "afr (provided,computed):" <+> ppr afr <+> ppr computed_afr
+               , pp_inputs ])
+  where
+    computed_afl = chooseFunTyFlag argl_ty resl_ty
+    computed_afr = chooseFunTyFlag argr_ty resr_ty
+    Pair argl_ty argr_ty = coercionKind arg_co
+    Pair resl_ty resr_ty = coercionKind res_co
+
+    pp_inputs = vcat [ pp_ty "argl" argl_ty, pp_ty "argr" argr_ty
+                     , pp_ty "resl" resl_ty, pp_ty "resr" resr_ty
+                     , text "arg_co:" <+> ppr arg_co
+                     , text "res_co:" <+> ppr res_co ]
+
+    ok ty = isTYPEorCONSTRAINT (typeKind ty)
+    pp_ty str ty = text str <> colon <+> hang (ppr ty)
+                                            2 (dcolon <+> ppr (typeKind ty))
 
 -- | Apply a 'Coercion' to another 'Coercion'.
 -- The second coercion must be Nominal, unless the first is Phantom.
@@ -899,11 +942,11 @@ mkForAllCo v kind_co co
 mkForAllCo_NoRefl :: TyCoVar -> CoercionN -> Coercion -> Coercion
 mkForAllCo_NoRefl v kind_co co
   | assert (varType v `eqType` (coercionLKind kind_co)) True
-  , assert (isTyVar v || almostDevoidCoVarOfCo v co) True
   , assert (not (isReflCo co)) True
   , isCoVar v
+  , assert (almostDevoidCoVarOfCo v co) True
   , not (v `elemVarSet` tyCoVarsOfCo co)
-  = FunCo (coercionRole co) (multToCo Many) kind_co co
+  = mkFunCoNoFTF (coercionRole co) (multToCo ManyTy) kind_co co
       -- Functions from coercions are always unrestricted
   | otherwise
   = ForAllCo v kind_co co
@@ -1064,142 +1107,84 @@ mkTransCo (GRefl r t1 (MCo co1)) (GRefl _ _ (MCo co2))
   = GRefl r t1 (MCo $ mkTransCo co1 co2)
 mkTransCo co1 co2                = TransCo co1 co2
 
-mkNthCo :: HasDebugCallStack
-        => Role  -- The role of the coercion you're creating
-        -> Int   -- Zero-indexed
+mkSelCo :: HasDebugCallStack
+        => CoSel
+        -> Coercion
         -> Coercion
+mkSelCo n co = mkSelCo_maybe n co `orElse` SelCo n co
+
+mkSelCo_maybe :: HasDebugCallStack
+        => CoSel
         -> Coercion
-mkNthCo r n co
-  = assertPpr good_call bad_call_msg $
-    go n co
+        -> Maybe Coercion
+-- mkSelCo_maybe tries to optimise call to mkSelCo
+mkSelCo_maybe cs co
+  = assertPpr (good_call cs) bad_call_msg $
+    go cs co
   where
     Pair ty1 ty2 = coercionKind co
 
-    go 0 co
-      | Just (ty, _) <- isReflCo_maybe co
-      , Just (tv, _) <- splitForAllTyCoVar_maybe ty
-      = -- works for both tyvar and covar
-        assert (r == Nominal) $
-        mkNomReflCo (varType tv)
-
-    go n co
-      | Just (ty, r0) <- isReflCo_maybe co
-      , let tc = tyConAppTyCon ty
-      = assertPpr (ok_tc_app ty n) (ppr n $$ ppr ty) $
-        assert (nthRole r0 tc n == r) $
-        mkReflCo r (tyConAppArgN n ty)
-      where ok_tc_app :: Type -> Int -> Bool
-            ok_tc_app ty n
-              | Just (_, tys) <- splitTyConApp_maybe ty
-              = tys `lengthExceeds` n
-              | isForAllTy ty  -- nth:0 pulls out a kind coercion from a hetero forall
-              = n == 0
-              | otherwise
-              = False
-
-    go 0 (ForAllCo _ kind_co _)
-      = assert (r == Nominal)
-        kind_co
+    go cs co
+      | Just (ty, r) <- isReflCo_maybe co
+      = Just (mkReflCo r (getNthFromType cs ty))
+
+    go SelForAll (ForAllCo _ kind_co _)
+      = Just kind_co
       -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
-      -- then (nth 0 co :: k1 ~N k2)
+      -- then (nth SelForAll co :: k1 ~N k2)
       -- If co :: (forall a1:t1 ~ t2. t1) ~ (forall a2:t3 ~ t4. t2)
-      -- then (nth 0 co :: (t1 ~ t2) ~N (t3 ~ t4))
+      -- then (nth SelForAll co :: (t1 ~ t2) ~N (t3 ~ t4))
 
-    go n (FunCo _ w arg res)
-      = mkNthCoFunCo n w arg res
+    go (SelFun fs) (FunCo _ _ _ w arg res)
+      = Just (getNthFun fs w arg res)
 
-    go n (TyConAppCo r0 tc arg_cos) = assertPpr (r == nthRole r0 tc n)
-                                                  (vcat [ ppr tc
-                                                        , ppr arg_cos
-                                                        , ppr r0
-                                                        , ppr n
-                                                        , ppr r ]) $
-                                             arg_cos `getNth` n
+    go (SelTyCon i r) (TyConAppCo r0 tc arg_cos)
+      = assertPpr (r == tyConRole r0 tc i)
+                  (vcat [ ppr tc, ppr arg_cos, ppr r0, ppr i, ppr r ]) $
+        Just (arg_cos `getNth` i)
 
-    go n (SymCo co)  -- Recurse, hoping to get to a TyConAppCo or FunCo
-      = mkSymCo (go n co)
+    go cs (SymCo co)  -- Recurse, hoping to get to a TyConAppCo or FunCo
+      = do { co' <- go cs co; return (mkSymCo co') }
 
-    go n co
-      = NthCo r n co
+    go _ _ = Nothing
 
     -- Assertion checking
     bad_call_msg = vcat [ text "Coercion =" <+> ppr co
                         , text "LHS ty =" <+> ppr ty1
                         , text "RHS ty =" <+> ppr ty2
-                        , text "n =" <+> ppr n, text "r =" <+> ppr r
+                        , text "cs =" <+> ppr cs
                         , text "coercion role =" <+> ppr (coercionRole co) ]
-    good_call
-      -- If the Coercion passed in is between forall-types, then the Int must
-      -- be 0 and the role must be Nominal.
+
+    -- good_call checks the typing rules given in Note [SelCo]
+    good_call SelForAll
       | Just (_tv1, _) <- splitForAllTyCoVar_maybe ty1
       , Just (_tv2, _) <- splitForAllTyCoVar_maybe ty2
-      = n == 0 && r == Nominal
-
-      -- If the Coercion passed in is between T tys and T tys', then the Int
-      -- must be less than the length of tys/tys' (which must be the same
-      -- lengths).
-      --
-      -- If the role of the Coercion is nominal, then the role passed in must
-      -- be nominal. If the role of the Coercion is representational, then the
-      -- role passed in must be tyConRolesRepresentational T !! n. If the role
-      -- of the Coercion is Phantom, then the role passed in must be Phantom.
-      --
-      -- See also Note [NthCo Cached Roles] if you're wondering why it's
-      -- blaringly obvious that we should be *computing* this role instead of
-      -- passing it in.
-      | Just (tc1, tys1) <- splitTyConApp_maybe ty1
-      , Just (tc2, tys2) <- splitTyConApp_maybe ty2
-      , tc1 == tc2
-      = let len1 = length tys1
-            len2 = length tys2
-            good_role = case coercionRole co of
-                          Nominal -> r == Nominal
-                          Representational -> r == (tyConRolesRepresentational tc1 !! n)
-                          Phantom -> r == Phantom
-        in len1 == len2 && n < len1 && good_role
+      =  True
 
-      | otherwise
-      = True
+    good_call (SelFun {})
+       = isFunTy ty1 && isFunTy ty2
 
--- | Extract the nth field of a FunCo
-mkNthCoFunCo :: Int         -- ^ "n"
-             -> CoercionN   -- ^ multiplicity coercion
-             -> Coercion    -- ^ argument coercion
-             -> Coercion    -- ^ result coercion
-             -> Coercion    -- ^ nth coercion from a FunCo
--- See Note [Function coercions]
--- If FunCo _ mult arg_co res_co ::   (s1:TYPE sk1 :mult-> s2:TYPE sk2)
---                                  ~ (t1:TYPE tk1 :mult-> t2:TYPE tk2)
--- Then we want to behave as if co was
---    TyConAppCo mult argk_co resk_co arg_co res_co
--- where
---    argk_co :: sk1 ~ tk1  =  mkNthCo 0 (mkKindCo arg_co)
---    resk_co :: sk2 ~ tk2  =  mkNthCo 0 (mkKindCo res_co)
---                             i.e. mkRuntimeRepCo
-mkNthCoFunCo n w co1 co2 = case n of
-  0 -> w
-  1 -> mkRuntimeRepCo co1
-  2 -> mkRuntimeRepCo co2
-  3 -> co1
-  4 -> co2
-  _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr w $$ ppr co1 $$ ppr co2)
-
--- | If you're about to call @mkNthCo r n co@, then @r@ should be
--- whatever @nthCoRole n co@ returns.
-nthCoRole :: Int -> Coercion -> Role
-nthCoRole n co
-  | Just (tc, _) <- splitTyConApp_maybe lty
-  = nthRole r tc n
-
-  | Just _ <- splitForAllTyCoVar_maybe lty
-  = Nominal
+    good_call (SelTyCon n r)
+       | Just (tc1, tys1) <- splitTyConApp_maybe ty1
+       , Just (tc2, tys2) <- splitTyConApp_maybe ty2
+       , let { len1 = length tys1
+             ; len2 = length tys2 }
+       =  tc1 == tc2
+       && len1 == len2
+       && n < len1
+       && r == tyConRole (coercionRole co) tc1 n
 
-  | otherwise
-  = pprPanic "nthCoRole" (ppr co)
+    good_call _ = False
 
-  where
-    lty = coercionLKind co
-    r   = coercionRole co
+-- | Extract the nth field of a FunCo
+getNthFun :: FunSel
+          -> a    -- ^ multiplicity
+          -> a    -- ^ argument
+          -> a    -- ^ result
+          -> a    -- ^ One of the above three
+getNthFun SelMult mult _   _   = mult
+getNthFun SelArg _     arg _   = arg
+getNthFun SelRes _     _   res = res
 
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
 mkLRCo lr co
@@ -1209,7 +1194,7 @@ mkLRCo lr co
   = LRCo lr co
 
 -- | Instantiates a 'Coercion'.
-mkInstCo :: Coercion -> Coercion -> Coercion
+mkInstCo :: Coercion -> CoercionN -> Coercion
 mkInstCo (ForAllCo tcv _kind_co body_co) co
   | Just (arg, _) <- isReflCo_maybe co
       -- works for both tyvar and covar
@@ -1225,7 +1210,7 @@ mkGReflRightCo r ty co
     -- instead of @isReflCo@
   | otherwise = GRefl r ty (MCo co)
 
--- | Given @ty :: k1@, @co :: k1 ~ k2@,
+-- | Given @r@, @ty :: k1@, and @co :: k1 ~N k2@,
 -- produces @co' :: (ty |> co) ~r ty@
 mkGReflLeftCo :: Role -> Type -> CoercionN -> Coercion
 mkGReflLeftCo r ty co
@@ -1277,10 +1262,10 @@ mkSubCo (Refl ty) = GRefl Representational ty MRefl
 mkSubCo (GRefl Nominal ty co) = GRefl Representational ty co
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
-mkSubCo (FunCo Nominal w arg res)
-  = FunCo Representational w
-          (downgradeRole Representational Nominal arg)
-          (downgradeRole Representational Nominal res)
+mkSubCo co@(FunCo { fco_role = Nominal, fco_arg = arg, fco_res = res })
+  = co { fco_role = Representational
+       , fco_arg = downgradeRole Representational Nominal arg
+       , fco_res = downgradeRole Representational Nominal res }
 mkSubCo co = assertPpr (coercionRole co == Nominal) (ppr co <+> ppr (coercionRole co)) $
              SubCo co
 
@@ -1350,10 +1335,11 @@ setNominalRole_maybe r co
     setNominalRole_maybe_helper (TyConAppCo Representational tc cos)
       = do { cos' <- zipWithM setNominalRole_maybe (tyConRolesX Representational tc) cos
            ; return $ TyConAppCo Nominal tc cos' }
-    setNominalRole_maybe_helper (FunCo Representational w co1 co2)
+    setNominalRole_maybe_helper co@(FunCo { fco_role = Representational
+                                          , fco_arg = co1, fco_res = co2 })
       = do { co1' <- setNominalRole_maybe Representational co1
            ; co2' <- setNominalRole_maybe Representational co2
-           ; return $ FunCo Nominal w co1' co2'
+           ; return $ co { fco_role = Nominal, fco_arg = co1', fco_res = co2' }
            }
     setNominalRole_maybe_helper (SymCo co)
       = SymCo <$> setNominalRole_maybe_helper co
@@ -1363,10 +1349,10 @@ setNominalRole_maybe r co
       = AppCo <$> setNominalRole_maybe_helper co1 <*> pure co2
     setNominalRole_maybe_helper (ForAllCo tv kind_co co)
       = ForAllCo tv kind_co <$> setNominalRole_maybe_helper co
-    setNominalRole_maybe_helper (NthCo _r n co)
+    setNominalRole_maybe_helper (SelCo n co)
       -- NB, this case recurses via setNominalRole_maybe, not
       -- setNominalRole_maybe_helper!
-      = NthCo Nominal n <$> setNominalRole_maybe (coercionRole co) co
+      = SelCo n <$> setNominalRole_maybe (coercionRole co) co
     setNominalRole_maybe_helper (InstCo co arg)
       = InstCo <$> setNominalRole_maybe_helper co <*> pure arg
     setNominalRole_maybe_helper (UnivCo prov _ co1 co2)
@@ -1395,7 +1381,7 @@ applyRoles :: TyCon -> [Coercion] -> [Coercion]
 applyRoles tc cos
   = zipWith (\r -> downgradeRole r Nominal) (tyConRolesRepresentational tc) cos
 
--- the Role parameter is the Role of the TyConAppCo
+-- The Role parameter is the Role of the TyConAppCo
 -- defined here because this is intimately concerned with the implementation
 -- of TyConAppCo
 -- Always returns an infinite list (with a infinite tail of Nominal)
@@ -1408,11 +1394,20 @@ tyConRolesX role             _  = repeat role
 tyConRolesRepresentational :: TyCon -> [Role]
 tyConRolesRepresentational tc = tyConRoles tc ++ repeat Nominal
 
-nthRole :: Role -> TyCon -> Int -> Role
-nthRole Nominal _ _ = Nominal
-nthRole Phantom _ _ = Phantom
-nthRole Representational tc n
-  = (tyConRolesRepresentational tc) `getNth` n
+tyConRole :: Role -> TyCon -> Int -> Role
+tyConRole Nominal          _  _ = Nominal
+tyConRole Phantom          _  _ = Phantom
+tyConRole Representational tc n = tyConRolesRepresentational tc `getNth` n
+
+funRole :: Role -> FunSel -> Role
+funRole Nominal          _  = Nominal
+funRole Phantom          _  = Phantom
+funRole Representational fs = funRoleRepresentational fs
+
+funRoleRepresentational :: FunSel -> Role
+funRoleRepresentational SelMult = Nominal
+funRoleRepresentational SelArg  = Representational
+funRoleRepresentational SelRes  = Representational
 
 ltRole :: Role -> Role -> Bool
 -- Is one role "less" than another?
@@ -1432,20 +1427,18 @@ promoteCoercion :: Coercion -> CoercionN
 -- First cases handles anything that should yield refl.
 promoteCoercion co = case co of
 
-    _ | ki1 `eqType` ki2
-      -> mkNomReflCo (typeKind ty1)
-     -- no later branch should return refl
-     --    The assert (False )s throughout
-     -- are these cases explicitly, but they should never fire.
-
-    Refl _ -> assert False $
-              mkNomReflCo ki1
+    Refl _ -> mkNomReflCo ki1
 
-    GRefl _ _ MRefl -> assert False $
-                       mkNomReflCo ki1
+    GRefl _ _ MRefl -> mkNomReflCo ki1
 
     GRefl _ _ (MCo co) -> co
 
+    _ | ki1 `eqType` ki2
+      -> mkNomReflCo (typeKind ty1)
+     -- No later branch should return refl
+     -- The assert (False )s throughout
+     -- are these cases explicitly, but they should never fire.
+
     TyConAppCo _ tc args
       | Just co' <- instCoercions (mkNomReflCo (tyConKind tc)) args
       -> co'
@@ -1463,14 +1456,19 @@ promoteCoercion co = case co of
       | isTyVar tv
       -> promoteCoercion g
 
-    ForAllCo _ _ _
+    ForAllCo {}
       -> assert False $
+            -- (ForAllCo {} :: (forall cv.t1) ~ (forall cv.t2)
+            -- The tyvar case is handled above, so the bound var is a
+            -- a coercion variable. So both sides have kind Type
+            -- (Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep).
+            -- So the result is Refl, and that should have been caught by
+            -- the first equation above
          mkNomReflCo liftedTypeKind
-      -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
-    FunCo _ _ _ _
-      -> assert False $
-         mkNomReflCo liftedTypeKind
+    FunCo {} -> mkKindCo co
+       -- We can get Type~Constraint or Constraint~Type
+       -- from FunCo {} :: (a -> (b::Type)) ~ (a -=> (b'::Constraint))
 
     CoVarCo {}     -> mkKindCo co
     HoleCo {}      -> mkKindCo co
@@ -1488,14 +1486,9 @@ promoteCoercion co = case co of
     TransCo co1 co2
       -> mkTransCo (promoteCoercion co1) (promoteCoercion co2)
 
-    NthCo _ n co1
-      | Just (_, args) <- splitTyConAppCo_maybe co1
-      , args `lengthExceeds` n
-      -> promoteCoercion (args !! n)
-
-      | Just _ <- splitForAllCo_maybe co
-      , n == 0
-      -> assert False $ mkNomReflCo liftedTypeKind
+    SelCo n co1
+      | Just co' <- mkSelCo_maybe n co1
+      -> promoteCoercion co'
 
       | otherwise
       -> mkKindCo co
@@ -1519,7 +1512,7 @@ promoteCoercion co = case co of
            -- See Note [Weird typing rule for ForAllTy] in GHC.Core.TyCo.Rep
 
     KindCo _
-      -> assert False $
+      -> assert False $ -- See the first equation above
          mkNomReflCo liftedTypeKind
 
     SubCo g
@@ -1547,10 +1540,12 @@ instCoercion (Pair lty rty) g w
     -- w :: s1 ~ s2
     -- returns mkInstCo g w' :: t2 [t1 |-> s1 ] ~ t3 [t1 |-> s2]
   = Just $ mkInstCo g w'
+
   | isFunTy lty && isFunTy rty
     -- g :: (t1 -> t2) ~ (t3 -> t4)
     -- returns t2 ~ t4
-  = Just $ mkNthCo Nominal 4 g -- extract result type, which is the 5th argument to (->)
+  = Just $ mkSelCo (SelFun SelRes) g -- extract result type
+
   | otherwise -- one forall, one funty...
   = Nothing
 
@@ -1619,17 +1614,18 @@ mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
                   -- want it to be r. It is only called in 'mkPiCos', which is
                   -- only used in GHC.Core.Opt.Simplify.Utils, where we are sure for
                   -- now (Aug 2018) v won't occur in co.
-                            mkFunResCo r scaled_ty co
-              | otherwise = mkFunResCo r scaled_ty co
-              where
-                scaled_ty = Scaled (varMult v) (varType v)
+                            mkFunResCo r v co
+              | otherwise = mkFunResCo r v co
 
-mkFunResCo :: Role -> Scaled Type -> Coercion -> Coercion
--- Given res_co :: res1 -> res2,
+mkFunResCo :: Role -> Id -> Coercion -> Coercion
+-- Given res_co :: res1 ~ res2,
 --   mkFunResCo r m arg res_co :: (arg -> res1) ~r (arg -> res2)
 -- Reflexive in the multiplicity argument
-mkFunResCo role (Scaled mult arg_ty) res_co
-  = mkFunCo role (multToCo mult) (mkReflCo role arg_ty) res_co
+mkFunResCo role id res_co
+  = mkFunCoNoFTF role mult arg_co res_co
+  where
+    arg_co = mkReflCo role (varType id)
+    mult   = multToCo (varMult id)
 
 -- mkCoCast (c :: s1 ~?r t1) (g :: (s1 ~?r t1) ~#R (s2 ~?r t2)) :: s2 ~?r t2
 -- The first coercion might be lifted or unlifted; thus the ~? above
@@ -1835,7 +1831,7 @@ The KPUSH rule deals with this situation
 We want to push the coercion inside the constructor application.
 So we do this
 
-   g' :: t1~t2  =  Nth 0 g
+   g' :: t1~t2  =  SelCo (SelTyCon 0) g
 
    case K @t2 (x |> g' -> Maybe g') of
      K (y:t2 -> Maybe t2) -> rhs
@@ -1852,7 +1848,7 @@ available at www.cis.upenn.edu/~sweirich/papers/fckinds-extended.pdf
 Note [extendLiftingContextEx]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~
 Consider we have datatype
-  K :: \/k. \/a::k. P -> T k  -- P be some type
+  K :: /\k. /\a::k. P -> T k  -- P be some type
   g :: T k1 ~ T k2
 
   case (K @k1 @t1 x) |> g of
@@ -1860,7 +1856,7 @@ Consider we have datatype
 
 We want to push the coercion inside the constructor application.
 We first get the coercion mapped by the universal type variable k:
-   lc = k |-> Nth 0 g :: k1~k2
+   lc = k |-> SelCo (SelTyCon 0) g :: k1~k2
 
 Here, the important point is that the kind of a is coerced, and P might be
 dependent on the existential type variable a.
@@ -2027,14 +2023,14 @@ ty_co_subst !lc role ty
   = go role ty
   where
     go :: Role -> Type -> Coercion
-    go r ty                | Just ty' <- coreView ty
-                           = go r ty'
-    go Phantom ty          = lift_phantom ty
-    go r (TyVarTy tv)      = expectJust "ty_co_subst bad roles" $
-                             liftCoSubstTyVar lc r tv
-    go r (AppTy ty1 ty2)   = mkAppCo (go r ty1) (go Nominal ty2)
-    go r (TyConApp tc tys) = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
-    go r (FunTy _ w ty1 ty2) = mkFunCo r (go Nominal w) (go r ty1) (go r ty2)
+    go r ty                 | Just ty' <- coreView ty
+                            = go r ty'
+    go Phantom ty           = lift_phantom ty
+    go r (TyVarTy tv)       = expectJust "ty_co_subst bad roles" $
+                              liftCoSubstTyVar lc r tv
+    go r (AppTy ty1 ty2)    = mkAppCo (go r ty1) (go Nominal ty2)
+    go r (TyConApp tc tys)  = mkTyConAppCo r tc (zipWith go (tyConRolesX r tc) tys)
+    go r (FunTy af w t1 t2) = mkFunCo1 r af (go Nominal w) (go r t1) (go r t2)
     go r t@(ForAllTy (Bndr v _) ty)
        = let (lc', v', h) = liftCoSubstVarBndr lc v
              body_co = ty_co_subst lc' r ty in
@@ -2192,8 +2188,8 @@ liftCoSubstCoVarBndrUsing view_co fun lc@(LC subst cenv) old_var
 
     role   = coVarRole old_var
     eta'   = downgradeRole role Nominal eta
-    eta1   = mkNthCo role 2 eta'
-    eta2   = mkNthCo role 3 eta'
+    eta1   = mkSelCo (SelTyCon 2 role) eta'
+    eta2   = mkSelCo (SelTyCon 3 role) eta'
 
     co1     = mkCoVarCo new_var
     co2     = mkSymCo eta1 `mkTransCo` co1 `mkTransCo` eta2
@@ -2285,7 +2281,8 @@ seqCo (TyConAppCo r tc cos)     = r `seq` tc `seq` seqCos cos
 seqCo (AppCo co1 co2)           = seqCo co1 `seq` seqCo co2
 seqCo (ForAllCo tv k co)        = seqType (varType tv) `seq` seqCo k
                                                        `seq` seqCo co
-seqCo (FunCo r w co1 co2)       = r `seq` seqCo w `seq` seqCo co1 `seq` seqCo co2
+seqCo (FunCo r af1 af2 w co1 co2) = r `seq` af1 `seq` af2 `seq`
+                                    seqCo w `seq` seqCo co1 `seq` seqCo co2
 seqCo (CoVarCo cv)              = cv `seq` ()
 seqCo (HoleCo h)                = coHoleCoVar h `seq` ()
 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
@@ -2293,7 +2290,7 @@ seqCo (UnivCo p r t1 t2)
   = seqProv p `seq` r `seq` seqType t1 `seq` seqType t2
 seqCo (SymCo co)                = seqCo co
 seqCo (TransCo co1 co2)         = seqCo co1 `seq` seqCo co2
-seqCo (NthCo r n co)            = r `seq` n `seq` seqCo co
+seqCo (SelCo n co)              = n `seq` seqCo co
 seqCo (LRCo lr co)              = lr `seq` seqCo co
 seqCo (InstCo co arg)           = seqCo co `seq` seqCo arg
 seqCo (KindCo co)               = seqCo co
@@ -2344,25 +2341,26 @@ coercionLKind :: Coercion -> Type
 coercionLKind co
   = go co
   where
-    go (Refl ty)                = ty
-    go (GRefl _ ty _)           = ty
-    go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
-    go (AppCo co1 co2)          = mkAppTy (go co1) (go co2)
-    go (ForAllCo tv1 _ co1)     = mkTyCoInvForAllTy tv1 (go co1)
-    go (FunCo _ w co1 co2)      = mkFunctionType (go w) (go co1) (go co2)
-    go (CoVarCo cv)             = coVarLType cv
-    go (HoleCo h)               = coVarLType (coHoleCoVar h)
-    go (UnivCo _ _ ty1 _)       = ty1
-    go (SymCo co)               = coercionRKind co
-    go (TransCo co1 _)          = go co1
-    go (LRCo lr co)             = pickLR lr (splitAppTy (go co))
-    go (InstCo aco arg)         = go_app aco [go arg]
-    go (KindCo co)              = typeKind (go co)
-    go (SubCo co)               = go co
-    go (NthCo _ d co)           = go_nth d (go co)
-    go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
-    go (AxiomRuleCo ax cos)     = pFst $ expectJust "coercionKind" $
-                                  coaxrProves ax $ map coercionKind cos
+    go (Refl ty)                 = ty
+    go (GRefl _ ty _)            = ty
+    go (TyConAppCo _ tc cos)     = mkTyConApp tc (map go cos)
+    go (AppCo co1 co2)           = mkAppTy (go co1) (go co2)
+    go (ForAllCo tv1 _ co1)      = mkTyCoInvForAllTy tv1 (go co1)
+    go (FunCo _ afl _ w co1 co2) = FunTy { ft_af = afl, ft_arg = go co1, ft_res = go co2
+                                         , ft_mult = go w }
+    go (CoVarCo cv)              = coVarLType cv
+    go (HoleCo h)                = coVarLType (coHoleCoVar h)
+    go (UnivCo _ _ ty1 _)        = ty1
+    go (SymCo co)                = coercionRKind co
+    go (TransCo co1 _)           = go co1
+    go (LRCo lr co)              = pickLR lr (splitAppTy (go co))
+    go (InstCo aco arg)          = go_app aco [go arg]
+    go (KindCo co)               = typeKind (go co)
+    go (SubCo co)                = go co
+    go (SelCo d co)              = getNthFromType d (go co)
+    go (AxiomInstCo ax ind cos)  = go_ax_inst ax ind (map go cos)
+    go (AxiomRuleCo ax cos)      = pFst $ expectJust "coercionKind" $
+                                   coaxrProves ax $ map coercionKind cos
 
     go_ax_inst ax ind tys
       | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
@@ -2382,42 +2380,47 @@ coercionLKind co
     go_app (InstCo co arg) args = go_app co (go arg:args)
     go_app co              args = piResultTys (go co) args
 
-go_nth :: Int -> Type -> Type
-go_nth d ty
+getNthFromType :: HasDebugCallStack => CoSel -> Type -> Type
+getNthFromType (SelFun fs) ty
+  | Just (_af, mult, arg, res) <- splitFunTy_maybe ty
+  = getNthFun fs mult arg res
+
+getNthFromType (SelTyCon n _) ty
   | Just args <- tyConAppArgs_maybe ty
-  = assert (args `lengthExceeds` d) $
-    args `getNth` d
+  = assertPpr (args `lengthExceeds` n) (ppr n $$ ppr ty) $
+    args `getNth` n
 
-  | d == 0
-  , Just (tv,_) <- splitForAllTyCoVar_maybe ty
+getNthFromType SelForAll ty       -- Works for both tyvar and covar
+  | Just (tv,_) <- splitForAllTyCoVar_maybe ty
   = tyVarKind tv
 
-  | otherwise
-  = pprPanic "coercionLKind:nth" (ppr d <+> ppr ty)
+getNthFromType cs ty
+  = pprPanic "getNthFromType" (ppr cs $$ ppr ty)
 
 coercionRKind :: Coercion -> Type
 coercionRKind co
   = go co
   where
-    go (Refl ty)                = ty
-    go (GRefl _ ty MRefl)       = ty
-    go (GRefl _ ty (MCo co1))   = mkCastTy ty co1
-    go (TyConAppCo _ tc cos)    = mkTyConApp tc (map go cos)
-    go (AppCo co1 co2)          = mkAppTy (go co1) (go co2)
-    go (CoVarCo cv)             = coVarRType cv
-    go (HoleCo h)               = coVarRType (coHoleCoVar h)
-    go (FunCo _ w co1 co2)      = mkFunctionType (go w) (go co1) (go co2)
-    go (UnivCo _ _ _ ty2)       = ty2
-    go (SymCo co)               = coercionLKind co
-    go (TransCo _ co2)          = go co2
-    go (LRCo lr co)             = pickLR lr (splitAppTy (go co))
-    go (InstCo aco arg)         = go_app aco [go arg]
-    go (KindCo co)              = typeKind (go co)
-    go (SubCo co)               = go co
-    go (NthCo _ d co)           = go_nth d (go co)
-    go (AxiomInstCo ax ind cos) = go_ax_inst ax ind (map go cos)
-    go (AxiomRuleCo ax cos)     = pSnd $ expectJust "coercionKind" $
-                                  coaxrProves ax $ map coercionKind cos
+    go (Refl ty)                 = ty
+    go (GRefl _ ty MRefl)        = ty
+    go (GRefl _ ty (MCo co1))    = mkCastTy ty co1
+    go (TyConAppCo _ tc cos)     = mkTyConApp tc (map go cos)
+    go (AppCo co1 co2)           = mkAppTy (go co1) (go co2)
+    go (CoVarCo cv)              = coVarRType cv
+    go (HoleCo h)                = coVarRType (coHoleCoVar h)
+    go (FunCo _ _ afr w co1 co2) = FunTy { ft_af = afr, ft_arg = go co1, ft_res = go co2
+                                         , ft_mult = go w }
+    go (UnivCo _ _ _ ty2)        = ty2
+    go (SymCo co)                = coercionLKind co
+    go (TransCo _ co2)           = go co2
+    go (LRCo lr co)              = pickLR lr (splitAppTy (go co))
+    go (InstCo aco arg)          = go_app aco [go arg]
+    go (KindCo co)               = typeKind (go co)
+    go (SubCo co)                = go co
+    go (SelCo d co)              = getNthFromType d (go co)
+    go (AxiomInstCo ax ind cos)  = go_ax_inst ax ind (map go cos)
+    go (AxiomRuleCo ax cos)      = pSnd $ expectJust "coercionKind" $
+                                   coaxrProves ax $ map coercionKind cos
 
     go co@(ForAllCo tv1 k_co co1) -- works for both tyvar and covar
        | isGReflCo k_co           = mkTyCoInvForAllTy tv1 (go co1)
@@ -2459,10 +2462,11 @@ coercionRKind co
       | isCoVar cv1
       = mkTyCoInvForAllTy cv2 (go_forall subst' co)
       where
-        k2 = coercionRKind k_co
-        r         = coVarRole cv1
-        eta1      = mkNthCo r 2 (downgradeRole r Nominal k_co)
-        eta2      = mkNthCo r 3 (downgradeRole r Nominal k_co)
+        k2    = coercionRKind k_co
+        r     = coVarRole cv1
+        k_co' = downgradeRole r Nominal k_co
+        eta1  = mkSelCo (SelTyCon 2 r) k_co'
+        eta2  = mkSelCo (SelTyCon 3 r) k_co'
 
         -- k_co :: (t1 ~r t2) ~N (s1 ~r s2)
         -- k1    = t1 ~r t2
@@ -2509,14 +2513,16 @@ coercionRole = go
     go (TyConAppCo r _ _) = r
     go (AppCo co1 _) = go co1
     go (ForAllCo _ _ co) = go co
-    go (FunCo r _ _ _) = r
+    go (FunCo { fco_role = r }) = r
     go (CoVarCo cv) = coVarRole cv
     go (HoleCo h)   = coVarRole (coHoleCoVar h)
     go (AxiomInstCo ax _ _) = coAxiomRole ax
     go (UnivCo _ r _ _)  = r
     go (SymCo co) = go co
     go (TransCo co1 _co2) = go co1
-    go (NthCo r _d _co) = r
+    go (SelCo SelForAll      _co) = Nominal
+    go (SelCo (SelTyCon _ r) _co) = r
+    go (SelCo (SelFun fs)     co) = funRole (coercionRole co) fs
     go (LRCo {}) = Nominal
     go (InstCo co _) = go co
     go (KindCo {}) = Nominal
@@ -2610,9 +2616,10 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
                   ; _           -> False      }) $
         mkNomReflCo ty1
 
-    go (FunTy { ft_mult = w1, ft_arg = arg1, ft_res = res1 })
-       (FunTy { ft_mult = w2, ft_arg = arg2, ft_res = res2 })
-      = mkFunCo Nominal (go w1 w2) (go arg1 arg2) (go res1 res2)
+    go (FunTy { ft_af = af1, ft_mult = w1, ft_arg = arg1, ft_res = res1 })
+       (FunTy { ft_af = af2, ft_mult = w2, ft_arg = arg2, ft_res = res2 })
+      = assert (af1 == af2) $
+        mkFunCo1 Nominal af1 (go w1 w2) (go arg1 arg2) (go res1 res2)
 
     go (TyConApp tc1 args1) (TyConApp tc2 args2)
       = assert (tc1 == tc2) $
@@ -2651,8 +2658,8 @@ buildCoercion orig_ty1 orig_ty2 = go orig_ty1 orig_ty2
 
             r    = coVarRole cv1
             kind_co' = downgradeRole r Nominal kind_co
-            eta1 = mkNthCo r 2 kind_co'
-            eta2 = mkNthCo r 3 kind_co'
+            eta1 = mkSelCo (SelTyCon 2 r) kind_co'
+            eta2 = mkSelCo (SelTyCon 3 r) kind_co'
 
             subst = mkEmptySubst $ mkInScopeSet $
                       tyCoVarsOfType ty2 `unionVarSet` tyCoVarsOfCo kind_co

compiler/GHC/Core/Coercion.hs-boot

@@ -17,14 +17,16 @@ mkReflCo :: Role -> Type -> Coercion
 mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkAppCo :: Coercion -> Coercion -> Coercion
 mkForAllCo :: TyCoVar -> Coercion -> Coercion -> Coercion
-mkFunCo :: Role -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo1 :: HasDebugCallStack => Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkNakedFunCo1 :: Role -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
+mkFunCo2 :: HasDebugCallStack => Role -> FunTyFlag -> FunTyFlag -> CoercionN -> Coercion -> Coercion -> Coercion
 mkCoVarCo :: CoVar -> Coercion
 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
 mkUnivCo :: UnivCoProvenance -> Role -> Type -> Type -> Coercion
 mkSymCo :: Coercion -> Coercion
 mkTransCo :: Coercion -> Coercion -> Coercion
-mkNthCo :: HasDebugCallStack => Role -> Int -> Coercion -> Coercion
+mkSelCo :: HasDebugCallStack => CoSel -> Coercion -> Coercion
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
 mkInstCo :: Coercion -> Coercion -> Coercion
 mkGReflCo :: Role -> Type -> MCoercionN -> Coercion

compiler/GHC/Core/Coercion/Opt.hs

 -- (c) The University of Glasgow 2006
 
-{-# LANGUAGE CPP #-}
+{-# LANGUAGE CPP, MultiWayIf #-}
 
 module GHC.Core.Coercion.Opt
    ( optCoercion
@@ -15,6 +15,7 @@ import GHC.Tc.Utils.TcType   ( exactTyCoVarsOfType )
 
 import GHC.Core.TyCo.Rep
 import GHC.Core.TyCo.Subst
+import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.Coercion
 import GHC.Core.Type as Type hiding( substTyVarBndr, substTy )
 import GHC.Core.TyCon
@@ -23,6 +24,7 @@ import GHC.Core.Unify
 
 import GHC.Types.Var.Set
 import GHC.Types.Var.Env
+import GHC.Types.Unique.Set
 
 import GHC.Data.Pair
 import GHC.Data.List.SetOps ( getNth )
@@ -123,8 +125,19 @@ optCoercion :: OptCoercionOpts -> Subst -> Coercion -> NormalCo
 -- ^ optCoercion applies a substitution to a coercion,
 --   *and* optimises it to reduce its size
 optCoercion opts env co
-  | optCoercionEnabled opts = optCoercion' env co
-  | otherwise               = substCo env co
+  | optCoercionEnabled opts
+  = optCoercion' env co
+{-
+  = pprTrace "optCoercion {" (text "Co:" <+> ppr co) $
+    let result = optCoercion' env co in
+    pprTrace "optCoercion }" (vcat [ text "Co:" <+> ppr co
+                                   , text "Optco:" <+> ppr result ]) $
+    result
+-}
+
+  | otherwise
+  = substCo env co
+
 
 optCoercion' :: Subst -> Coercion -> NormalCo
 optCoercion' env co
@@ -136,19 +149,23 @@ optCoercion' env co
     assertPpr (substTyUnchecked env in_ty1 `eqType` out_ty1 &&
                substTyUnchecked env in_ty2 `eqType` out_ty2 &&
                in_role == out_role)
-              ( text "optCoercion changed types!"
-                 $$ hang (text "in_co:") 2 (ppr co)
-                 $$ hang (text "in_ty1:") 2 (ppr in_ty1)
-                 $$ hang (text "in_ty2:") 2 (ppr in_ty2)
-                 $$ hang (text "out_co:") 2 (ppr out_co)
-                 $$ hang (text "out_ty1:") 2 (ppr out_ty1)
-                 $$ hang (text "out_ty2:") 2 (ppr out_ty2)
-                 $$ hang (text "subst:") 2 (ppr env))
-              out_co
+              (hang (text "optCoercion changed types!")
+                  2 (vcat [ text "in_co:" <+> ppr co
+                          , text "in_ty1:" <+> ppr in_ty1
+                          , text "in_ty2:" <+> ppr in_ty2
+                          , text "out_co:" <+> ppr out_co
+                          , text "out_ty1:" <+> ppr out_ty1
+                          , text "out_ty2:" <+> ppr out_ty2
+                          , text "in_role:" <+> ppr in_role
+                          , text "out_role:" <+> ppr out_role
+                          , vcat $ map ppr_one $ nonDetEltsUniqSet $ coVarsOfCo co
+                          , text "subst:" <+> ppr env ]))
+               out_co
 
   | otherwise         = opt_co1 lc False co
   where
     lc = mkSubstLiftingContext env
+    ppr_one cv = ppr cv <+> dcolon <+> ppr (coVarKind cv)
 
 
 type NormalCo    = Coercion
@@ -191,9 +208,12 @@ opt_co3 env sym _                       r co = opt_co4_wrap env sym False r co
 
 -- See Note [Optimising coercion optimisation]
 -- | Optimize a non-phantom coercion.
-opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag -> Role -> Coercion -> NormalCo
-
+opt_co4, opt_co4_wrap :: LiftingContext -> SymFlag -> ReprFlag
+                      -> Role -> Coercion -> NormalCo
+-- Precondition: In every call (opt_co4 lc sym rep role co)
+--               we should have role = coercionRole co
 opt_co4_wrap = opt_co4
+
 {-
 opt_co4_wrap env sym rep r co
   = pprTrace "opt_co4_wrap {"
@@ -201,12 +221,13 @@ opt_co4_wrap env sym rep r co
            , text "Rep:" <+> ppr rep
            , text "Role:" <+> ppr r
            , text "Co:" <+> ppr co ]) $
-    assert (r == coercionRole co )
+    assert (r == coercionRole co )    $
     let result = opt_co4 env sym rep r co in
     pprTrace "opt_co4_wrap }" (ppr co $$ text "---" $$ ppr result) $
     result
 -}
 
+
 opt_co4 env _   rep r (Refl ty)
   = assertPpr (r == Nominal)
               (text "Expected role:" <+> ppr r    $$
@@ -269,15 +290,17 @@ opt_co4 env sym rep r (ForAllCo tv k_co co)
                             opt_co4_wrap env' sym rep r co
      -- Use the "mk" functions to check for nested Refls
 
-opt_co4 env sym rep r (FunCo _r cow co1 co2)
+opt_co4 env sym rep r (FunCo _r afl afr cow co1 co2)
   = assert (r == _r) $
-    if rep
-    then mkFunCo Representational cow' co1' co2'
-    else mkFunCo r cow' co1' co2'
+    mkFunCo2 r' afl' afr' cow' co1' co2'
   where
     co1' = opt_co4_wrap env sym rep r co1
     co2' = opt_co4_wrap env sym rep r co2
     cow' = opt_co1 env sym cow
+    !r' | rep       = Representational
+        | otherwise = r
+    !(afl', afr') | sym       = (afr,afl)
+                  | otherwise = (afl,afr)
 
 opt_co4 env sym rep r (CoVarCo cv)
   | Just co <- lookupCoVar (lcSubst env) cv
@@ -333,38 +356,29 @@ opt_co4 env sym rep r (TransCo co1 co2)
     co2' = opt_co4_wrap env sym rep r co2
     in_scope = lcInScopeSet env
 
-opt_co4 env _sym rep r (NthCo _r n co)
-  | Just (ty, _) <- isReflCo_maybe co
-  , Just (_tc, args) <- assert (r == _r )
-                        splitTyConApp_maybe ty
-  = liftCoSubst (chooseRole rep r) env (args `getNth` n)
-
-  | Just (ty, _) <- isReflCo_maybe co
-  , n == 0
-  , Just (tv, _) <- splitForAllTyCoVar_maybe ty
-      -- works for both tyvar and covar
-  = liftCoSubst (chooseRole rep r) env (varType tv)
+opt_co4 env _sym rep r (SelCo n co)
+  | Just (ty, _co_role) <- isReflCo_maybe co
+  = liftCoSubst (chooseRole rep r) env (getNthFromType n ty)
+    -- NB: it is /not/ true that r = _co_role
+    --     Rather, r = coercionRole (SelCo n co)
 
-opt_co4 env sym rep r (NthCo r1 n (TyConAppCo _ _ cos))
+opt_co4 env sym rep r (SelCo (SelTyCon n r1) (TyConAppCo _ _ cos))
   = assert (r == r1 )
     opt_co4_wrap env sym rep r (cos `getNth` n)
 
 -- see the definition of GHC.Builtin.Types.Prim.funTyCon
-opt_co4 env sym rep r (NthCo r1 n (FunCo _r2 w co1 co2))
-  = assert (r == r1 )
-    opt_co4_wrap env sym rep r (mkNthCoFunCo n w co1 co2)
+opt_co4 env sym rep r (SelCo (SelFun fs) (FunCo _r2 _afl _afr w co1 co2))
+  = opt_co4_wrap env sym rep r (getNthFun fs w co1 co2)
 
-opt_co4 env sym rep r (NthCo _r n (ForAllCo _ eta _))
+opt_co4 env sym rep _ (SelCo SelForAll (ForAllCo _ eta _))
       -- works for both tyvar and covar
-  = assert (r == _r )
-    assert (n == 0 )
-    opt_co4_wrap env sym rep Nominal eta
-
-opt_co4 env sym rep r (NthCo _r n co)
-  | Just nth_co <- case co' of
-      TyConAppCo _ _ cos -> Just (cos `getNth` n)
-      FunCo _ w co1 co2  -> Just (mkNthCoFunCo n w co1 co2)
-      ForAllCo _ eta _   -> Just eta
+  = opt_co4_wrap env sym rep Nominal eta
+
+opt_co4 env sym rep r (SelCo n co)
+  | Just nth_co <- case (co', n) of
+      (TyConAppCo _ _ cos, SelTyCon n _) -> Just (cos `getNth` n)
+      (FunCo _ _ _ w co1 co2, SelFun fs) -> Just (getNthFun fs w co1 co2)
+      (ForAllCo _ eta _, SelForAll)      -> Just eta
       _                  -> Nothing
   = if rep && (r == Nominal)
       -- keep propagating the SubCo
@@ -372,7 +386,7 @@ opt_co4 env sym rep r (NthCo _r n co)
     else nth_co
 
   | otherwise
-  = wrapRole rep r $ NthCo r n co'
+  = wrapRole rep r $ SelCo n co'
   where
     co' = opt_co1 env sym co
 
@@ -455,8 +469,8 @@ opt_co4 env sym rep r (InstCo co1 arg)
             -- new_co = (h1 :: t1 ~ t2) ~ ((n1;h2;sym n2) :: t1 ~ t2)
             r2  = coVarRole cv
             kind_co' = downgradeRole r2 Nominal kind_co
-            n1 = mkNthCo r2 2 kind_co'
-            n2 = mkNthCo r2 3 kind_co'
+            n1 = mkSelCo (SelTyCon 2 r2) kind_co'
+            n2 = mkSelCo (SelTyCon 3 r2) kind_co'
          in mkProofIrrelCo Nominal (Refl (coercionType h1)) h1
                            (n1 `mkTransCo` h2 `mkTransCo` (mkSymCo n2))
 
@@ -577,9 +591,9 @@ opt_univ env sym prov role oty1 oty2
         eta   = mkUnivCo prov' Nominal k1 k2
         eta_d = downgradeRole r' Nominal eta
           -- eta gets opt'ed soon, but not yet.
-        n_co  = (mkSymCo $ mkNthCo r' 2 eta_d) `mkTransCo`
+        n_co  = (mkSymCo $ mkSelCo (SelTyCon 2 r') eta_d) `mkTransCo`
                 (mkCoVarCo cv1) `mkTransCo`
-                (mkNthCo r' 3 eta_d)
+                (mkSelCo (SelTyCon 3 r') eta_d)
         ty2'  = substTyWithCoVars [cv2] [n_co] ty2
 
         (env', cv1', eta') = optForAllCoBndr env sym cv1 eta
@@ -651,13 +665,12 @@ opt_trans_rule is in_co1@(GRefl r1 t1 (MCo co1)) in_co2@(GRefl r2 _ (MCo co2))
     mkGReflRightCo r1 t1 (opt_trans is co1 co2)
 
 -- Push transitivity through matching destructors
-opt_trans_rule is in_co1@(NthCo r1 d1 co1) in_co2@(NthCo r2 d2 co2)
+opt_trans_rule is in_co1@(SelCo d1 co1) in_co2@(SelCo d2 co2)
   | d1 == d2
   , coercionRole co1 == coercionRole co2
   , co1 `compatible_co` co2
-  = assert (r1 == r2) $
-    fireTransRule "PushNth" in_co1 in_co2 $
-    mkNthCo r1 d1 (opt_trans is co1 co2)
+  = fireTransRule "PushNth" in_co1 in_co2 $
+    mkSelCo d1 (opt_trans is co1 co2)
 
 opt_trans_rule is in_co1@(LRCo d1 co1) in_co2@(LRCo d2 co2)
   | d1 == d2
@@ -694,10 +707,14 @@ opt_trans_rule is in_co1@(TyConAppCo r1 tc1 cos1) in_co2@(TyConAppCo r2 tc2 cos2
     fireTransRule "PushTyConApp" in_co1 in_co2 $
     mkTyConAppCo r1 tc1 (opt_transList is cos1 cos2)
 
-opt_trans_rule is in_co1@(FunCo r1 w1 co1a co1b) in_co2@(FunCo r2 w2 co2a co2b)
-  = assert (r1 == r2) $   -- Just like the TyConAppCo/TyConAppCo case
+opt_trans_rule is in_co1@(FunCo r1 afl1 afr1 w1 co1a co1b)
+                  in_co2@(FunCo r2 afl2 afr2 w2 co2a co2b)
+  = assert (r1 == r2)     $     -- Just like the TyConAppCo/TyConAppCo case
+    assert (afr1 == afl2) $
     fireTransRule "PushFun" in_co1 in_co2 $
-    mkFunCo r1 (opt_trans is w1 w2) (opt_trans is co1a co2a) (opt_trans is co1b co2b)
+    mkFunCo2 r1 afl1 afr2 (opt_trans is w1 w2)
+                          (opt_trans is co1a co2a)
+                          (opt_trans is co1b co2b)
 
 opt_trans_rule is in_co1@(AppCo co1a co1b) in_co2@(AppCo co2a co2b)
   -- Must call opt_trans_rule_app; see Note [EtaAppCo]
@@ -772,8 +789,8 @@ opt_trans_rule is co1 co2
       is'  = is `extendInScopeSet` cv1
       role = coVarRole cv1
       eta1' = downgradeRole role Nominal eta1
-      n1   = mkNthCo role 2 eta1'
-      n2   = mkNthCo role 3 eta1'
+      n1   = mkSelCo (SelTyCon 2 role) eta1'
+      n2   = mkSelCo (SelTyCon 3 role) eta1'
       r2'  = substCo (zipCvSubst [cv2] [(mkSymCo n1) `mkTransCo`
                                         (mkCoVarCo cv1) `mkTransCo` n2])
                     r2
@@ -1134,9 +1151,9 @@ Similarly, we do this
 
 Here,
 
-  h1   = mkNthCo Nominal 0 g :: (s1~s2)~(s3~s4)
-  eta1 = mkNthCo r 2 h1      :: (s1 ~ s3)
-  eta2 = mkNthCo r 3 h1      :: (s2 ~ s4)
+  h1   = mkSelCo Nominal 0 g       :: (s1~s2)~(s3~s4)
+  eta1 = mkSelCo (SelTyCon 2 r) h1 :: (s1 ~ s3)
+  eta2 = mkSelCo (SelTyCon 3 r) h1 :: (s2 ~ s4)
   h2   = mkInstCo g (cv1 ~ (sym eta1;c1;eta2))
 -}
 etaForAllCo_ty_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
@@ -1148,7 +1165,7 @@ etaForAllCo_ty_maybe co
   | Pair ty1 ty2  <- coercionKind co
   , Just (tv1, _) <- splitForAllTyVar_maybe ty1
   , isForAllTy_ty ty2
-  , let kind_co = mkNthCo Nominal 0 co
+  , let kind_co = mkSelCo SelForAll co
   = Just ( tv1, kind_co
          , mkInstCo co (mkGReflRightCo Nominal (TyVarTy tv1) kind_co))
 
@@ -1164,13 +1181,13 @@ etaForAllCo_co_maybe co
   | Pair ty1 ty2  <- coercionKind co
   , Just (cv1, _) <- splitForAllCoVar_maybe ty1
   , isForAllTy_co ty2
-  = let kind_co  = mkNthCo Nominal 0 co
+  = let kind_co  = mkSelCo SelForAll co
         r        = coVarRole cv1
         l_co     = mkCoVarCo cv1
         kind_co' = downgradeRole r Nominal kind_co
-        r_co     = (mkSymCo (mkNthCo r 2 kind_co')) `mkTransCo`
-                   l_co `mkTransCo`
-                   (mkNthCo r 3 kind_co')
+        r_co     = mkSymCo (mkSelCo (SelTyCon 2 r) kind_co')
+                   `mkTransCo` l_co
+                   `mkTransCo` mkSelCo (SelTyCon 3 r) kind_co'
     in Just ( cv1, kind_co
             , mkInstCo co (mkProofIrrelCo Nominal kind_co l_co r_co))
 
@@ -1197,17 +1214,19 @@ etaAppCo_maybe co
 etaTyConAppCo_maybe :: TyCon -> Coercion -> Maybe [Coercion]
 -- If possible, split a coercion
 --       g :: T s1 .. sn ~ T t1 .. tn
--- into [ Nth 0 g :: s1~t1, ..., Nth (n-1) g :: sn~tn ]
+-- into [ SelCo (SelTyCon 0)     g :: s1~t1
+--      , ...
+--      , SelCo (SelTyCon (n-1)) g :: sn~tn ]
 etaTyConAppCo_maybe tc (TyConAppCo _ tc2 cos2)
   = assert (tc == tc2) $ Just cos2
 
 etaTyConAppCo_maybe tc co
-  | not (mustBeSaturated tc)
+  | not (tyConMustBeSaturated tc)
   , (Pair ty1 ty2, r) <- coercionKindRole co
   , Just (tc1, tys1)  <- splitTyConApp_maybe ty1
   , Just (tc2, tys2)  <- splitTyConApp_maybe ty2
   , tc1 == tc2
-  , isInjectiveTyCon tc r  -- See Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
+  , isInjectiveTyCon tc r  -- See Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
   , let n = length tys1
   , tys2 `lengthIs` n      -- This can fail in an erroneous program
                            -- E.g. T a ~# T a b

compiler/GHC/Core/ConLike.hs

@@ -185,10 +185,14 @@ conLikeResTy (PatSynCon ps)    tys = patSynInstResTy ps tys
 --
 -- 7) The original result type
 conLikeFullSig :: ConLike
-               -> ([TyVar], [TyCoVar], [EqSpec]
+               -> ([TyVar], [TyCoVar]
                    -- Why tyvars for universal but tycovars for existential?
                    -- See Note [Existential coercion variables] in GHC.Core.DataCon
-                  , ThetaType, ThetaType, [Scaled Type], Type)
+                  , [EqSpec]
+                  , ThetaType      -- Provided theta
+                  , ThetaType      -- Required theta
+                  , [Scaled Type]  -- Arguments
+                  , Type )         -- Result
 conLikeFullSig (RealDataCon con) =
   let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, res_ty) = dataConFullSig con
   -- Required theta is empty as normal data cons require no additional

compiler/GHC/Core/DataCon.hs

@@ -20,7 +20,6 @@ module GHC.Core.DataCon (
         -- ** Equality specs
         EqSpec, mkEqSpec, eqSpecTyVar, eqSpecType,
         eqSpecPair, eqSpecPreds,
-        substEqSpec, filterEqSpec,
 
         -- ** Field labels
         FieldLabel(..), FieldLabelString,
@@ -37,11 +36,11 @@ module GHC.Core.DataCon (
         dataConDisplayType,
         dataConUnivTyVars, dataConExTyCoVars, dataConUnivAndExTyCoVars,
         dataConUserTyVars, dataConUserTyVarBinders,
-        dataConEqSpec, dataConTheta,
+        dataConTheta,
         dataConStupidTheta,
         dataConOtherTheta,
         dataConInstArgTys, dataConOrigArgTys, dataConOrigResTy,
-        dataConInstOrigArgTys, dataConRepArgTys,
+        dataConInstOrigArgTys, dataConRepArgTys, dataConResRepTyArgs,
         dataConInstUnivs,
         dataConFieldLabels, dataConFieldType, dataConFieldType_maybe,
         dataConSrcBangs,
@@ -56,10 +55,10 @@ module GHC.Core.DataCon (
         -- ** Predicates on DataCons
         isNullarySrcDataCon, isNullaryRepDataCon,
         isTupleDataCon, isBoxedTupleDataCon, isUnboxedTupleDataCon,
-        isUnboxedSumDataCon,
+        isUnboxedSumDataCon, isCovertGadtDataCon,
         isVanillaDataCon, isNewDataCon, isTypeDataCon,
         classDataCon, dataConCannotMatch,
-        dataConUserTyVarsArePermuted,
+        dataConUserTyVarsNeedWrapper, checkDataConTyVars,
         isBanged, isMarkedStrict, cbvFromStrictMark, eqHsBang, isSrcStrict, isSrcUnpacked,
         specialPromotedDc,
 
@@ -77,6 +76,7 @@ import GHC.Core.Coercion
 import GHC.Core.Unify
 import GHC.Core.TyCon
 import GHC.Core.TyCo.Subst
+import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.Multiplicity
 import {-# SOURCE #-} GHC.Types.TyThing
 import GHC.Types.FieldLabel
@@ -94,7 +94,7 @@ import GHC.Utils.Binary
 import GHC.Types.Unique.FM ( UniqFM )
 import GHC.Types.Unique.Set
 import GHC.Builtin.Uniques( mkAlphaTyVarUnique )
-
+import GHC.Data.Graph.UnVar  -- UnVarSet and operations
 
 import GHC.Utils.Outputable
 import GHC.Utils.Misc
@@ -422,7 +422,7 @@ data DataCon
                 --       syntax, provided its type looks like the above.
                 --       The declaration format is held in the TyCon (algTcGadtSyntax)
 
-        -- Universally-quantified type vars [a,b,c]
+        -- dcUnivTyVars: Universally-quantified type vars [a,b,c]
         -- INVARIANT: length matches arity of the dcRepTyCon
         -- INVARIANT: result type of data con worker is exactly (T a b c)
         -- COROLLARY: The dcUnivTyVars are always in one-to-one correspondence with
@@ -431,16 +431,16 @@ data DataCon
 
         -- Existentially-quantified type and coercion vars [x,y]
         -- For an example involving coercion variables,
-        -- Why tycovars? See Note [Existential coercion variables]
+        -- Why TyCoVars? See Note [Existential coercion variables]
         dcExTyCoVars     :: [TyCoVar],
 
         -- INVARIANT: the UnivTyVars and ExTyCoVars all have distinct OccNames
         -- Reason: less confusing, and easier to generate Iface syntax
 
         -- The type/coercion vars in the order the user wrote them [c,y,x,b]
-        -- INVARIANT: the set of tyvars in dcUserTyVarBinders is exactly the set
-        --            of tyvars (*not* covars) of dcExTyCoVars unioned with the
-        --            set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
+        -- INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders is
+        --    exactly the set of tyvars (*not* covars) of dcExTyCoVars unioned
+        --    with the set of dcUnivTyVars whose tyvars do not appear in dcEqSpec
         -- See Note [DataCon user type variable binders]
         dcUserTyVarBinders :: [InvisTVBinder],
 
@@ -553,7 +553,7 @@ For the TyVarBinders in a DataCon and PatSyn:
 
  * Each argument flag is Inferred or Specified.
    None are Required. (A DataCon is a term-level function; see
-   Note [No Required TyCoBinder in terms] in GHC.Core.TyCo.Rep.)
+   Note [No Required PiTyBinder in terms] in GHC.Core.TyCo.Rep.)
 
 Why do we need the TyVarBinders, rather than just the TyVars?  So that
 we can construct the right type for the DataCon with its foralls
@@ -565,23 +565,23 @@ order in which TyVarBinders appear in a DataCon.
 
 Note [Existential coercion variables]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-
 For now (Aug 2018) we can't write coercion quantifications in source Haskell, but
 we can in Core. Consider having:
 
   data T :: forall k. k -> k -> Constraint where
-    MkT :: forall k (a::k) (b::k). forall k' (c::k') (co::k'~k). (b~(c|>co))
-        => T k a b
+    MkT :: forall k (a::k) (b::k).
+           forall k' (c::k') (co::k'~k).
+           (b ~# (c|>co)) => T k a b
 
   dcUnivTyVars       = [k,a,b]
   dcExTyCoVars       = [k',c,co]
   dcUserTyVarBinders = [k,a,k',c]
-  dcEqSpec           = [b~(c|>co)]
+  dcEqSpec           = [b ~# (c|>co)]
   dcOtherTheta       = []
   dcOrigArgTys       = []
   dcRepTyCon         = T
 
-  Function call 'dataConKindEqSpec' returns [k'~k]
+Function call 'dataConKindEqSpec' returns [k'~k]
 
 Note [DataCon arities]
 ~~~~~~~~~~~~~~~~~~~~~~
@@ -593,6 +593,31 @@ but dcRepArity does.  For example:
 
 Note [DataCon user type variable binders]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+A DataCon has two different sets of type variables:
+
+* dcUserTyVarBinders, for the type variables binders in the order in which they
+  originally arose in the user-written type signature.
+
+  - They are the forall'd binders of the data con /wrapper/, which the user calls.
+
+  - Their order *does* matter for TypeApplications, so they are full TyVarBinders,
+    complete with visibilities.
+
+* dcUnivTyVars and dcExTyCoVars, for the "true underlying" (i.e. of the data
+  con worker) universal type variable and existential type/coercion variables,
+  respectively.
+
+  - They (i.e. univ ++ ex) are the forall'd variables of the data con /worker/
+
+  - Their order is irrelevant for the purposes of TypeApplications,
+    and as a consequence, they do not come equipped with visibilities
+    (that is, they are TyVars/TyCoVars instead of ForAllTyBinders).
+
+Often (dcUnivTyVars ++ dcExTyCoVars) = dcUserTyVarBinders; but they may differ
+for three reasons, coming next:
+
+--- Reason (R1): Order of quantification in GADT syntax ---
+
 In System FC, data constructor type signatures always quantify over all of
 their universal type variables, followed by their existential type variables.
 Normally, this isn't a problem, as most datatypes naturally quantify their type
@@ -635,36 +660,119 @@ according to the rules of TypeApplications, in the absence of `forall` GHC
 performs a stable topological sort on the type variables in the user-written
 type signature, which would place `b` before `a`.
 
-But as noted above, enacting this behavior is not entirely trivial, as System
-FC demands the variables go in universal-then-existential order under the hood.
-Our solution is thus to equip DataCon with two different sets of type
-variables:
+--- Reason (R2): GADT constructors quantify over different variables ---
 
-* dcUnivTyVars and dcExTyCoVars, for the universal type variable and existential
-  type/coercion variables, respectively. Their order is irrelevant for the
-  purposes of TypeApplications, and as a consequence, they do not come equipped
-  with visibilities (that is, they are TyVars/TyCoVars instead of
-  TyCoVarBinders).
+GADT constructors may quantify over different variables than the worker
+would.  Consider
+   data T a b where
+      MkT :: forall c d. c -> T [c] d
 
-* dcUserTyVarBinders, for the type variables binders in the order in which they
-  originally arose in the user-written type signature. Their order *does* matter
-  for TypeApplications, so they are full TyVarBinders, complete with
-  visibilities.
+The dcUserTyVarBinders must be [c, d] -- that's what the user quantified over.
+But c is actually existential, as it is not equal to either of the two
+universal variables.
+
+Here is what we'll get:
+
+  dcUserTyVarBinders = [c, d]
+  dcUnivTyVars = [a, d]
+  dcExTyCoVars = [c]
+
+Note that dcUnivTyVars contains `a` from the type header (the `data T a b`)
+and `d` from the signature for MkT. This is done because d is used in place
+of b in the result of MkT, and so we use the name d for the universal, as that
+might improve error messages. On the other hand, we need to use a fresh name
+for the first universal (recalling that the result of a worker must be the
+type constructor applied to a sequence of plain variables), so we use `a`, from
+the header. This choice of universals is made in GHC.Tc.TyCl.mkGADTVars.
+
+Because c is not a universal, it is an existential. Here, we see that (even
+ignoring order) dcUserTyVarBinders is not dcUnivTyVars ⋃ dcExTyCoVars, because
+the latter has `a` while the former does not. To understand this better, let's
+look at this type for the "true underlying" worker data con:
+
+      MkT :: forall a d. forall c. (a ~# [c]) => c -> T a d
+
+We see here that the `a` universal is connected with the `c` existential via
+an equality constraint. It will always be the case (see the code in mkGADTVars)
+that the universals not mentioned in dcUserTyVarBinders will be used in a
+GADT equality -- that is, used on the left-hand side of an element of dcEqSpec:
+
+  dcEqSpec = [a ~# [c]]
+
+Putting this all together, all variables used on the left-hand side of an
+equation in the dcEqSpec will be in dcUnivTyVars but *not* in
+dcUserTyVarBinders.
+
+--- Reason (R3): Kind equalities may have been solved ---
+
+Consider now this case:
+
+  type family F a where
+    F Type = False
+    F _    = True
+  type T :: forall k. (F k ~ True) => k -> k -> Type
+  data T a b where
+    MkT :: T Maybe List
+
+The constraint F k ~ True tells us that T does not want to be indexed by, say,
+Int. Now let's consider the Core types involved:
+
+  axiom for F: axF[0] :: F Type ~ False
+               axF[1] :: forall a. F a ~ True   (a must be apart from Type)
+  tycon: T :: forall k. (F k ~ True) -> k -> k -> Type
+  wrapper: MkT :: T @(Type -> Type) @(Eq# (axF[1] (Type -> Type)) Maybe List
+  worker:  MkT :: forall k (c :: F k ~ True) (a :: k) (b :: k).
+                  (k ~# (Type -> Type), a ~# Maybe, b ~# List) =>
+                  T @k @c a b
+
+The key observation here is that the worker quantifies over c, while the wrapper
+does not. The worker *must* quantify over c, because c is a universal variable,
+and the result of the worker must be the type constructor applied to a sequence
+of plain type variables. But the wrapper certainly does not need to quantify over
+any evidence that F (Type -> Type) ~ True, as no variables are needed there.
+
+(Aside: the c here is a regular type variable, *not* a coercion variable. This
+is because F k ~ True is a *lifted* equality, not the unlifted ~#. This is why
+we see Eq# in the type of the wrapper: Eq# boxes the unlifted ~# to become a
+lifted ~. See also Note [The equality types story] in GHC.Builtin.Types.Prim about
+Eq# and Note [Constraints in kinds] in GHC.Core.TyCo.Rep about having this constraint
+in the first place.)
 
-This encoding has some redundancy. The set of tyvars in dcUserTyVarBinders
-consists precisely of:
+In this case, we'll have these fields of the DataCon:
+
+  dcUserTyVarBinders = []    -- the wrapper quantifies over nothing
+  dcUnivTyVars = [k, c, a, b]
+  dcExTyCoVars = []  -- no existentials here, but a different constructor might have
+  dcEqSpec = [k ~# (Type -> Type), a ~# Maybe, b ~# List]
+
+Note that c is in the dcUserTyVars, but mentioned neither in the dcUserTyVarBinders nor
+in the dcEqSpec. We thus have Reason (R3): a variable might be missing from the
+dcUserTyVarBinders if its type's kind is Constraint.
+
+(At one point, we thought that the dcEqSpec would have to be non-empty. But that
+wouldn't account for silly cases like type T :: (True ~ True) => Type.)
+
+--- End of Reasons ---
+
+INVARIANT(dataConTyVars): the set of tyvars in dcUserTyVarBinders
+consists of:
 
 * The set of tyvars in dcUnivTyVars whose type variables do not appear in
   dcEqSpec, unioned with:
+
 * The set of tyvars (*not* covars) in dcExTyCoVars
   No covars here because because they're not user-written
 
+When comparing for equality, we ignore differences concerning type variables
+whose kinds have kind Constraint.
+
 The word "set" is used above because the order in which the tyvars appear in
 dcUserTyVarBinders can be completely different from the order in dcUnivTyVars or
 dcExTyCoVars. That is, the tyvars in dcUserTyVarBinders are a permutation of
 (tyvars of dcExTyCoVars + a subset of dcUnivTyVars). But aside from the
 ordering, they in fact share the same type variables (with the same Uniques). We
-sometimes refer to this as "the dcUserTyVarBinders invariant".
+sometimes refer to this as "the dcUserTyVarBinders invariant". It is checked
+in checkDataConTyVars.
 
 dcUserTyVarBinders, as the name suggests, is the one that users will
 see most of the time. It's used when computing the type signature of a
@@ -767,8 +875,7 @@ data StrictnessMark = MarkedStrict | NotMarkedStrict
 
 -- | An 'EqSpec' is a tyvar/type pair representing an equality made in
 -- rejigging a GADT constructor
-data EqSpec = EqSpec TyVar
-                     Type
+data EqSpec = EqSpec TyVar Type
 
 -- | Make a non-dependent 'EqSpec'
 mkEqSpec :: TyVar -> Type -> EqSpec
@@ -787,22 +894,6 @@ eqSpecPreds :: [EqSpec] -> ThetaType
 eqSpecPreds spec = [ mkPrimEqPred (mkTyVarTy tv) ty
                    | EqSpec tv ty <- spec ]
 
--- | Substitute in an 'EqSpec'. Precondition: if the LHS of the EqSpec
--- is mapped in the substitution, it is mapped to a type variable, not
--- a full type.
-substEqSpec :: Subst -> EqSpec -> EqSpec
-substEqSpec subst (EqSpec tv ty)
-  = EqSpec tv' (substTy subst ty)
-  where
-    tv' = getTyVar "substEqSpec" (substTyVar subst tv)
-
--- | Filter out any 'TyVar's mentioned in an 'EqSpec'.
-filterEqSpec :: [EqSpec] -> [TyVar] -> [TyVar]
-filterEqSpec eq_spec
-  = filter not_in_eq_spec
-  where
-    not_in_eq_spec var = all (not . (== var) . eqSpecTyVar) eq_spec
-
 instance Outputable EqSpec where
   ppr (EqSpec tv ty) = ppr (tv, ty)
 
@@ -884,7 +975,7 @@ but the rep type is
 Actually, the unboxed part isn't implemented yet!
 
 Not that this representation is still *different* from runtime
-representation. (Which is what STG uses afer unarise).
+representation. (Which is what STG uses after unarise).
 
 This is how T would end up being used in STG post-unarise:
 
@@ -1047,7 +1138,7 @@ mkDataCon :: Name
           -> KnotTied ThetaType -- ^ Theta-type occurring before the arguments proper
           -> [KnotTied (Scaled Type)]    -- ^ Original argument types
           -> KnotTied Type      -- ^ Original result type
-          -> RuntimeRepInfo     -- ^ See comments on 'GHC.Core.TyCon.RuntimeRepInfo'
+          -> PromDataConInfo    -- ^ See comments on 'GHC.Core.TyCon.PromDataConInfo'
           -> KnotTied TyCon     -- ^ Representation type constructor
           -> ConTag             -- ^ Constructor tag
           -> ThetaType          -- ^ The "stupid theta", context of the data
@@ -1108,8 +1199,11 @@ mkDataCon name declared_infix prom_info
         -- If the DataCon has a wrapper, then the worker's type is never seen
         -- by the user. The visibilities we pick do not matter here.
         DCR{} -> mkInfForAllTys univ_tvs $ mkTyCoInvForAllTys ex_tvs $
-                 mkVisFunTys rep_arg_tys $
+                 mkScaledFunctionTys rep_arg_tys $
                  mkTyConApp rep_tycon (mkTyVarTys univ_tvs)
+                 -- res_arg_tys is a mixture of TypeLike and ConstraintLike,
+                 -- so we don't know which FunTyFlag to use
+                 -- Hence using mkScaledFunctionTys.
 
       -- See Note [Promoted data constructors] in GHC.Core.TyCon
     prom_tv_bndrs = [ mkNamedTyConBinder (Invisible spec) tv
@@ -1119,9 +1213,9 @@ mkDataCon name declared_infix prom_info
       -- fresh_names: make sure that the "anonymous" tyvars don't
       -- clash in name or unique with the universal/existential ones.
       -- Tiresome!  And unnecessary because these tyvars are never looked at
-    prom_theta_bndrs = [ mkAnonTyConBinder InvisArg (mkTyVar n t)
+    prom_theta_bndrs = [ mkInvisAnonTyConBinder (mkTyVar n t)
      {- Invisible -}   | (n,t) <- fresh_names `zip` theta ]
-    prom_arg_bndrs   = [ mkAnonTyConBinder VisArg (mkTyVar n t)
+    prom_arg_bndrs   = [ mkAnonTyConBinder (mkTyVar n t)
      {- Visible -}     | (n,t) <- dropList theta fresh_names `zip` map scaledThing orig_arg_tys ]
     prom_bndrs       = prom_tv_bndrs ++ prom_theta_bndrs ++ prom_arg_bndrs
     prom_res_kind    = orig_res_ty
@@ -1208,30 +1302,6 @@ dataConUserTyVars (MkData { dcUserTyVarBinders = tvbs }) = binderVars tvbs
 dataConUserTyVarBinders :: DataCon -> [InvisTVBinder]
 dataConUserTyVarBinders = dcUserTyVarBinders
 
--- | Equalities derived from the result type of the data constructor, as written
--- by the programmer in any GADT declaration. This includes *all* GADT-like
--- equalities, including those written in by hand by the programmer.
-dataConEqSpec :: DataCon -> [EqSpec]
-dataConEqSpec con@(MkData { dcEqSpec = eq_spec, dcOtherTheta = theta })
-  = dataConKindEqSpec con
-    ++ eq_spec ++
-    [ spec   -- heterogeneous equality
-    | Just (tc, [_k1, _k2, ty1, ty2]) <- map splitTyConApp_maybe theta
-    , tc `hasKey` heqTyConKey
-    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
-                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
-                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
-                    _             -> []
-    ] ++
-    [ spec   -- homogeneous equality
-    | Just (tc, [_k, ty1, ty2]) <- map splitTyConApp_maybe theta
-    , tc `hasKey` eqTyConKey
-    , spec <- case (getTyVar_maybe ty1, getTyVar_maybe ty2) of
-                    (Just tv1, _) -> [mkEqSpec tv1 ty2]
-                    (_, Just tv2) -> [mkEqSpec tv2 ty1]
-                    _             -> []
-    ]
-
 -- | Dependent (kind-level) equalities in a constructor.
 -- There are extracted from the existential variables.
 -- See Note [Existential coercion variables]
@@ -1247,7 +1317,7 @@ dataConKindEqSpec (MkData {dcExTyCoVars = ex_tcvs})
     | cv <- ex_tcvs
     , isCoVar cv
     , let (_, _, ty1, ty, _) = coVarKindsTypesRole cv
-          tv = getTyVar "dataConKindEqSpec" ty1
+          tv = getTyVar ty1
     ]
 
 -- | The *full* constraints on the constructor type, including dependent GADT
@@ -1467,18 +1537,18 @@ dataConWrapperType (MkData { dcUserTyVarBinders = user_tvbs,
                              dcOrigResTy = res_ty,
                              dcStupidTheta = stupid_theta })
   = mkInvisForAllTys user_tvbs $
-    mkInvisFunTysMany (stupid_theta ++ theta) $
-    mkVisFunTys arg_tys $
+    mkInvisFunTys (stupid_theta ++ theta) $
+    mkScaledFunTys arg_tys $
     res_ty
 
 dataConNonlinearType :: DataCon -> Type
 dataConNonlinearType (MkData { dcUserTyVarBinders = user_tvbs,
                                dcOtherTheta = theta, dcOrigArgTys = arg_tys,
                                dcOrigResTy = res_ty })
-  = let arg_tys' = map (\(Scaled w t) -> Scaled (case w of One -> Many; _ -> w) t) arg_tys
+  = let arg_tys' = map (\(Scaled w t) -> Scaled (case w of OneTy -> ManyTy; _ -> w) t) arg_tys
     in mkInvisForAllTys user_tvbs $
-       mkInvisFunTysMany theta $
-       mkVisFunTys arg_tys' $
+       mkInvisFunTys theta $
+       mkScaledFunTys arg_tys' $
        res_ty
 
 dataConDisplayType :: Bool -> DataCon -> Type
@@ -1595,7 +1665,7 @@ dataConRepArgTys (MkData { dcRep = rep
                          , dcOtherTheta = theta
                          , dcOrigArgTys = orig_arg_tys })
   = case rep of
-      NoDataConRep -> assert (null eq_spec) $ (map unrestricted theta) ++ orig_arg_tys
+      NoDataConRep -> assert (null eq_spec) $ map unrestricted theta ++ orig_arg_tys
       DCR { dcr_arg_tys = arg_tys } -> arg_tys
 
 -- | The string @package:module.name@ identifying a constructor, which is attached
@@ -1640,6 +1710,61 @@ isNewDataCon dc = isNewTyCon (dataConTyCon dc)
 isTypeDataCon :: DataCon -> Bool
 isTypeDataCon dc = isTcClsNameSpace (nameNameSpace (getName dc))
 
+isCovertGadtDataCon :: DataCon -> Bool
+-- See Note [isCovertGadtDataCon]
+isCovertGadtDataCon (MkData { dcUnivTyVars  = univ_tvs
+                            , dcEqSpec     = eq_spec
+                            , dcRepTyCon   = rep_tc })
+  =  not (null eq_spec)                -- There are some constraints
+  && not (any is_visible_spec eq_spec) -- But none of them are visible
+  where
+    visible_univ_tvs :: [TyVar]  -- Visible arguments in result type
+    visible_univ_tvs
+      = [ univ_tv | (univ_tv, tcb) <- univ_tvs `zip` tyConBinders rep_tc
+                  , isVisibleTyConBinder tcb ]
+
+    is_visible_spec :: EqSpec -> Bool
+    is_visible_spec (EqSpec univ_tv ty)
+       = univ_tv `elem` visible_univ_tvs
+         && not (isTyVarTy ty)  -- See Note [isCovertGadtDataCon] for
+                                -- an example where 'ty' is a tyvar
+
+{- Note [isCovertGadtDataCon]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+(isCovertGadtDataCon K) returns True if K is a GADT data constructor, but
+does not /look/ like it. Consider (#21447)
+    type T :: TYPE r -> Type
+    data T a where { MkT :: b -> T b }
+Here MkT doesn't look GADT-like, but it is. If we make the kind applications
+explicit we'd see:
+    data T a where { MkT :: b -> T @LiftedRep b }
+
+The test for covert-ness is bit tricky, because we want to see if
+  - dcEqSpec is non-empty
+  - dcEqSpec does not constrain any of the /required/ (i.e. visible)
+    arguments of the TyCon to a non-tyvar
+
+In the example above, the DataCon for MkT will have
+    dcUnivTyVars: [(r::RuntimeRep), (a :: TYPE r)]
+    dcExTyVars:   [(b :: Type)]
+    dcEqSpec:     [(r, LiftedRep), (a, b)]
+Here
+  * `r :: RuntimeRep` is constrained by dcEqSpec to LiftedRep
+  * `a :: TYPE r` is constrained by dcEqSpec to `b :: Type`
+But the constraint on `a` is not visible to the user, so this counts
+as a covert GADT data con.  The declaration
+     MkT :: forall (b :: Type). b -> T b
+looks entirely non-GADT-ish.
+
+Wrinkles:
+* The visibility or otherwise is a property of the /TyCon/ binders
+* The dcUnivTyVars may or may not be the same as the TyCon binders
+* So we have to zip them together.
+* For a data family the TyCon in question is the /representation/ TyCon
+  hence dcRepTyCon
+-}
+
+
 -- | Should this DataCon be allowed in a type even without -XDataKinds?
 -- Currently, only Lifted & Unlifted
 specialPromotedDc :: DataCon -> Bool
@@ -1680,17 +1805,71 @@ dataConCannotMatch tys con
 --
 -- This is not a cheap test, so we minimize its use in GHC as much as possible.
 -- Currently, its only call site in the GHC codebase is in 'mkDataConRep' in
--- "MkId", and so 'dataConUserTyVarsArePermuted' is only called at most once
+-- "MkId", and so 'dataConUserTyVarsNeedWrapper' is only called at most once
 -- during a data constructor's lifetime.
 
+dataConResRepTyArgs :: DataCon -> [Type]
+-- Returns the arguments of a GADT version of the /representation/ TyCon
+-- Thus   data instance T [(x,y)] z where
+--           MkT :: forall p q. Int -> T [(Int,p)] (Maybe q)
+-- The "GADT version of the representation type" is
+--        data R:T x y z where
+--           MkT :: forall p q. Int -> R:T Int p (Maybe q)
+-- so dataConResRepTyArgs for MkT returns [Int, p, Maybe q]
+-- This is almost the same as (subst eq_spec univ_tvs); but not quite,
+--   because eq_spec omits constraint-kinded equalities
+dataConResRepTyArgs dc@(MkData { dcRepTyCon = rep_tc, dcOrigResTy = orig_res_ty })
+  | Just (fam_tc, fam_args) <- tyConFamInst_maybe rep_tc
+  = -- fvs(fam_args) = tyConTyVars rep_tc
+    -- These tyvars are the domain of subst
+    -- Fvs(range(subst)) = tvars of the datacon
+    case  tcMatchTy (mkTyConApp fam_tc fam_args) orig_res_ty of
+       Just subst -> map (substTyVar subst) (tyConTyVars rep_tc)
+       Nothing    -> pprPanic "datacOnResRepTyArgs" $
+                     vcat [ ppr dc, ppr fam_tc <+> ppr fam_args
+                          , ppr orig_res_ty ]
+  | otherwise
+  = tyConAppArgs orig_res_ty
+
+checkDataConTyVars :: DataCon -> Bool
+-- Check that the worker and wrapper have the same set of type variables
+-- See Note [DataCon user type variable binders]
+-- Also ensures that no user tyvar is in the eq_spec (the eq_spec should
+-- only relate fresh universals from (R2) of the note)
+checkDataConTyVars dc@(MkData { dcUnivTyVars = univ_tvs
+                              , dcExTyCoVars = ex_tvs
+                              , dcEqSpec = eq_spec })
+     -- use of sets here: (R1) from the Note
+  = mkUnVarSet depleted_worker_vars == mkUnVarSet depleted_wrapper_vars &&
+    all (not . is_eq_spec_var) wrapper_vars
+  where
+    is_constraint_var v = typeTypeOrConstraint (tyVarKind v) == ConstraintLike
+      -- implements (R3) from the Note
+
+    worker_vars = univ_tvs ++ ex_tvs
+    eq_spec_tvs = mkUnVarSet (map eqSpecTyVar eq_spec)
+    is_eq_spec_var = (`elemUnVarSet` eq_spec_tvs)  -- (R2) from the Note
+    depleted_worker_vars = filterOut (is_eq_spec_var <||> is_constraint_var)
+                                     worker_vars
+
+    wrapper_vars = dataConUserTyVars dc
+    depleted_wrapper_vars = filterOut is_constraint_var wrapper_vars
+
+dataConUserTyVarsNeedWrapper :: DataCon -> Bool
+-- Check whether the worker and wapper have the same type variables
+-- in the same order. If not, we need a wrapper to swizzle them.
 -- See Note [DataCon user type variable binders], as well as
 -- Note [Data con wrappers and GADT syntax] for an explanation of what
 -- mkDataConRep is doing with this function.
-dataConUserTyVarsArePermuted :: DataCon -> Bool
-dataConUserTyVarsArePermuted (MkData { dcUnivTyVars = univ_tvs
-                                     , dcExTyCoVars = ex_tvs, dcEqSpec = eq_spec
-                                     , dcUserTyVarBinders = user_tvbs }) =
-  (filterEqSpec eq_spec univ_tvs ++ ex_tvs) /= binderVars user_tvbs
+dataConUserTyVarsNeedWrapper dc@(MkData { dcUnivTyVars = univ_tvs
+                                        , dcExTyCoVars = ex_tvs
+                                        , dcEqSpec = eq_spec })
+  = assert (null eq_spec || answer)  -- all GADTs should say "yes" here
+    answer
+  where
+    answer = (univ_tvs ++ ex_tvs) /= dataConUserTyVars dc
+              -- Worker tyvars         Wrapper tyvars
+
 
 {-
 %************************************************************************

compiler/GHC/Core/FVs.hs

@@ -72,7 +72,7 @@ import GHC.Core.TyCon
 import GHC.Core.Coercion.Axiom
 import GHC.Core.FamInstEnv
 import GHC.Builtin.Types( unrestrictedFunTyConName )
-import GHC.Builtin.Types.Prim( funTyConName )
+import GHC.Builtin.Types.Prim( fUNTyCon )
 import GHC.Data.Maybe( orElse )
 
 import GHC.Utils.FV as FV
@@ -349,19 +349,25 @@ orphNamesOfType ty | Just ty' <- coreView ty = orphNamesOfType ty'
                 -- Look through type synonyms (#4912)
 orphNamesOfType (TyVarTy _)          = emptyNameSet
 orphNamesOfType (LitTy {})           = emptyNameSet
+orphNamesOfType (ForAllTy bndr res)  = orphNamesOfType (binderType bndr)
+                                       `unionNameSet` orphNamesOfType res
 orphNamesOfType (TyConApp tycon tys) = func
                                        `unionNameSet` orphNamesOfTyCon tycon
                                        `unionNameSet` orphNamesOfTypes tys
         where func = case tys of
-                       arg:_ | tycon == funTyCon -> orph_names_of_fun_ty_con arg
+                       arg:_ | tycon == fUNTyCon -> orph_names_of_fun_ty_con arg
                        _ -> emptyNameSet
-orphNamesOfType (ForAllTy bndr res)  = orphNamesOfType (binderType bndr)
-                                       `unionNameSet` orphNamesOfType res
-orphNamesOfType (FunTy _ w arg res)  =  orph_names_of_fun_ty_con w
-                                       `unionNameSet` unitNameSet funTyConName
+
+orphNamesOfType (FunTy af w arg res) =  func
+                                       `unionNameSet` unitNameSet fun_tc
                                        `unionNameSet` orphNamesOfType w
                                        `unionNameSet` orphNamesOfType arg
                                        `unionNameSet` orphNamesOfType res
+        where func | isVisibleFunArg af = orph_names_of_fun_ty_con w
+                   | otherwise          = emptyNameSet
+
+              fun_tc = tyConName (funTyFlagTyCon af)
+
 orphNamesOfType (AppTy fun arg)      = orphNamesOfType fun `unionNameSet` orphNamesOfType arg
 orphNamesOfType (CastTy ty co)       = orphNamesOfType ty `unionNameSet` orphNamesOfCo co
 orphNamesOfType (CoercionTy co)      = orphNamesOfCo co
@@ -381,15 +387,19 @@ orphNamesOfCo (Refl ty)             = orphNamesOfType ty
 orphNamesOfCo (GRefl _ ty mco)      = orphNamesOfType ty `unionNameSet` orphNamesOfMCo mco
 orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` orphNamesOfCos cos
 orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (ForAllCo _ kind_co co)
-  = orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co
-orphNamesOfCo (FunCo _ co_mult co1 co2) = orphNamesOfCo co_mult `unionNameSet` orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
+orphNamesOfCo (ForAllCo _ kind_co co)     = orphNamesOfCo kind_co
+                                            `unionNameSet` orphNamesOfCo co
+orphNamesOfCo (FunCo { fco_mult = co_mult, fco_arg = co1, fco_res = co2 })
+                                    = orphNamesOfCo co_mult
+                                      `unionNameSet` orphNamesOfCo co1
+                                      `unionNameSet` orphNamesOfCo co2
 orphNamesOfCo (CoVarCo _)           = emptyNameSet
 orphNamesOfCo (AxiomInstCo con _ cos) = orphNamesOfCoCon con `unionNameSet` orphNamesOfCos cos
-orphNamesOfCo (UnivCo p _ t1 t2)    = orphNamesOfProv p `unionNameSet` orphNamesOfType t1 `unionNameSet` orphNamesOfType t2
+orphNamesOfCo (UnivCo p _ t1 t2)    = orphNamesOfProv p `unionNameSet` orphNamesOfType t1
+                                      `unionNameSet` orphNamesOfType t2
 orphNamesOfCo (SymCo co)            = orphNamesOfCo co
 orphNamesOfCo (TransCo co1 co2)     = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
-orphNamesOfCo (NthCo _ _ co)        = orphNamesOfCo co
+orphNamesOfCo (SelCo _ co)          = orphNamesOfCo co
 orphNamesOfCo (LRCo  _ co)          = orphNamesOfCo co
 orphNamesOfCo (InstCo co arg)       = orphNamesOfCo co `unionNameSet` orphNamesOfCo arg
 orphNamesOfCo (KindCo co)           = orphNamesOfCo co
@@ -437,8 +447,8 @@ orphNamesOfFamInst fam_inst = orphNamesOfAxiom (famInstAxiom fam_inst)
 -- Detect FUN 'Many as an application of (->), so that :i (->) works as expected
 -- (see #8535) Issue #16475 describes a more robust solution
 orph_names_of_fun_ty_con :: Mult -> NameSet
-orph_names_of_fun_ty_con Many = unitNameSet unrestrictedFunTyConName
-orph_names_of_fun_ty_con _ = emptyNameSet
+orph_names_of_fun_ty_con ManyTy = unitNameSet unrestrictedFunTyConName
+orph_names_of_fun_ty_con _      = emptyNameSet
 
 {-
 ************************************************************************
@@ -791,3 +801,4 @@ freeVars = go
 
     go (Type ty)     = (tyCoVarsOfTypeDSet ty, AnnType ty)
     go (Coercion co) = (tyCoVarsOfCoDSet co, AnnCoercion co)
+

compiler/GHC/Core/FamInstEnv.hs

@@ -42,6 +42,7 @@ import GHC.Prelude
 import GHC.Core.Unify
 import GHC.Core.Type as Type
 import GHC.Core.TyCo.Rep
+import GHC.Core.TyCo.Compare( eqType, eqTypes )
 import GHC.Core.TyCon
 import GHC.Core.Coercion
 import GHC.Core.Coercion.Axiom

compiler/GHC/Core/InstEnv.hs

@@ -38,15 +38,16 @@ import GHC.Tc.Utils.TcType -- InstEnv is really part of the type checker,
               -- and depends on TcType in many ways
 import GHC.Core ( IsOrphan(..), isOrphan, chooseOrphanAnchor )
 import GHC.Core.RoughMap
+import GHC.Core.Class
+import GHC.Core.Unify
+
 import GHC.Unit.Module.Env
 import GHC.Unit.Types
-import GHC.Core.Class
 import GHC.Types.Var
 import GHC.Types.Unique.DSet
 import GHC.Types.Var.Set
 import GHC.Types.Name
 import GHC.Types.Name.Set
-import GHC.Core.Unify
 import GHC.Types.Basic
 import GHC.Types.Id
 import Data.Data        ( Data )

compiler/GHC/Core/Lint.hs

@@ -49,9 +49,10 @@ import GHC.Core.Type as Type
 import GHC.Core.Multiplicity
 import GHC.Core.UsageEnv
 import GHC.Core.TyCo.Rep   -- checks validity of types/coercions
+import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.TyCo.Subst
 import GHC.Core.TyCo.FVs
-import GHC.Core.TyCo.Ppr ( pprTyVar, pprTyVars )
+import GHC.Core.TyCo.Ppr
 import GHC.Core.TyCon as TyCon
 import GHC.Core.Coercion.Axiom
 import GHC.Core.Unify
@@ -167,9 +168,10 @@ If we have done specialisation the we check that there are
 
 Note [Linting function types]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
-As described in Note [Representation of function types], all saturated
-applications of funTyCon are represented with the FunTy constructor. We check
-this invariant in lintType.
+All saturated applications of funTyCon are represented with the FunTy constructor.
+See Note [Function type constructors and FunTy] in GHC.Builtin.Types.Prim
+
+ We check this invariant in lintType.
 
 Note [Linting type lets]
 ~~~~~~~~~~~~~~~~~~~~~~~~
@@ -925,7 +927,7 @@ lintCoreExpr e@(Let (Rec pairs) body)
         ; ((body_type, body_ue), ues) <-
             lintRecBindings NotTopLevel pairs $ \ bndrs' ->
             lintLetBody bndrs' body
-        ; return (body_type, body_ue  `addUE` scaleUE Many (foldr1 addUE ues)) }
+        ; return (body_type, body_ue  `addUE` scaleUE ManyTy (foldr1 addUE ues)) }
   where
     bndrs = map fst pairs
 
@@ -1405,7 +1407,7 @@ lintTyApp fun_ty arg_ty
 -- application.
 lintValApp :: CoreExpr -> LintedType -> LintedType -> UsageEnv -> UsageEnv -> LintM (LintedType, UsageEnv)
 lintValApp arg fun_ty arg_ty fun_ue arg_ue
-  | Just (w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty
+  | Just (_, w, arg_ty', res_ty') <- splitFunTy_maybe fun_ty
   = do { ensureEqTys arg_ty' arg_ty (mkAppMsg arg_ty' arg_ty arg)
        ; let app_ue =  addUE fun_ue (scaleUE w arg_ue)
        ; return (res_ty', app_ue) }
@@ -1567,8 +1569,8 @@ lintCoreAlt case_bndr scrut_ty _scrut_mult alt_ty alt@(Alt (DataAlt con) args rh
         -- We've already check
       lintL (tycon == dataConTyCon con) (mkBadConMsg tycon con)
     ; let { con_payload_ty = piResultTys (dataConRepType con) tycon_arg_tys
-          ; binderMult (Named _)   = Many
-          ; binderMult (Anon _ st) = scaledMult st
+          ; binderMult (Named _)   = ManyTy
+          ; binderMult (Anon st _) = scaledMult st
           -- See Note [Validating multiplicities in a case]
           ; multiplicities = map binderMult $ fst $ splitPiTys con_payload_ty }
 
@@ -1637,19 +1639,25 @@ lintBinder site var linterF
 lintTyBndr :: TyVar -> (LintedTyCoVar -> LintM a) -> LintM a
 lintTyBndr = lintTyCoBndr  -- We could specialise it, I guess
 
--- lintCoBndr :: CoVar -> (LintedTyCoVar -> LintM a) -> LintM a
--- lintCoBndr = lintTyCoBndr  -- We could specialise it, I guess
-
 lintTyCoBndr :: TyCoVar -> (LintedTyCoVar -> LintM a) -> LintM a
 lintTyCoBndr tcv thing_inside
   = do { subst <- getSubst
-       ; kind' <- lintType (varType tcv)
+       ; tcv_type' <- lintType (varType tcv)
        ; let tcv' = uniqAway (getSubstInScope subst) $
-                    setVarType tcv kind'
+                    setVarType tcv tcv_type'
              subst' = extendTCvSubstWithClone subst tcv tcv'
-       ; when (isCoVar tcv) $
-         lintL (isCoVarType kind')
-               (text "CoVar with non-coercion type:" <+> pprTyVar tcv)
+
+       -- See (FORALL1) and (FORALL2) in GHC.Core.Type
+       ; if (isTyVar tcv)
+         then -- Check that in (forall (a:ki). blah) we have ki:Type
+              lintL (isLiftedTypeKind (typeKind tcv_type')) $
+              hang (text "TyVar whose kind does not have kind Type:")
+                 2 (ppr tcv' <+> dcolon <+> ppr tcv_type' <+> dcolon <+> ppr (typeKind tcv_type'))
+         else -- Check that in (forall (cv::ty). blah),
+              -- then ty looks like (t1 ~# t2)
+              lintL (isCoVarType tcv_type') $
+              text "CoVar with non-coercion type:" <+> pprTyVar tcv
+
        ; updateSubst subst' (thing_inside tcv') }
 
 lintIdBndrs :: forall a. TopLevelFlag -> [Id] -> ([LintedId] -> LintM a) -> LintM a
@@ -1731,7 +1739,7 @@ lintValueType ty
   = addLoc (InType ty) $
     do  { ty' <- lintType ty
         ; let sk = typeKind ty'
-        ; lintL (classifiesTypeWithValues sk) $
+        ; lintL (isTYPEorCONSTRAINT sk) $
           hang (text "Ill-kinded type:" <+> ppr ty)
              2 (text "has kind:" <+> ppr sk)
         ; return ty' }
@@ -1779,13 +1787,11 @@ lintType ty@(TyConApp tc tys)
   = do { report_unsat <- lf_report_unsat_syns <$> getLintFlags
        ; lintTySynFamApp report_unsat ty tc tys }
 
-  | isFunTyCon tc
-  , tys `lengthIs` 5
+  | Just {} <- tyConAppFunTy_maybe tc tys
     -- We should never see a saturated application of funTyCon; such
     -- applications should be represented with the FunTy constructor.
-    -- See Note [Linting function types] and
-    -- Note [Representation of function types].
-  = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty))
+    -- See Note [Linting function types]
+  = failWithL (hang (text "Saturated application of" <+> quotes (ppr tc)) 2 (ppr ty))
 
   | otherwise  -- Data types, data families, primitive types
   = do { checkTyCon tc
@@ -1800,6 +1806,12 @@ lintType ty@(FunTy af tw t1 t2)
        ; t2' <- lintType t2
        ; tw' <- lintType tw
        ; lintArrow (text "type or kind" <+> quotes (ppr ty)) t1' t2' tw'
+       ; let real_af = chooseFunTyFlag t1 t2
+       ; unless (real_af == af) $ addErrL $
+         hang (text "Bad FunTyFlag in FunTy")
+            2 (vcat [ ppr ty
+                    , text "FunTyFlag =" <+> ppr af
+                    , text "Computed FunTyFlag =" <+> ppr real_af ])
        ; return (FunTy af tw' t1' t2') }
 
 lintType ty@(ForAllTy (Bndr tcv vis) body_ty)
@@ -1888,7 +1900,7 @@ lintTySynFamApp report_unsat ty tc tys
 -- Confirms that a type is really TYPE r or Constraint
 checkValueType :: LintedType -> SDoc -> LintM ()
 checkValueType ty doc
-  = lintL (classifiesTypeWithValues kind)
+  = lintL (isTYPEorCONSTRAINT kind)
           (text "Non-Type-like kind when Type-like expected:" <+> ppr kind $$
            text "when checking" <+> doc)
   where
@@ -1900,17 +1912,16 @@ lintArrow :: SDoc -> LintedType -> LintedType -> LintedType -> LintM ()
 -- See Note [GHC Formalism]
 lintArrow what t1 t2 tw  -- Eg lintArrow "type or kind `blah'" k1 k2 kw
                          -- or lintArrow "coercion `blah'" k1 k2 kw
-  = do { unless (classifiesTypeWithValues k1) (addErrL (msg (text "argument") k1))
-       ; unless (classifiesTypeWithValues k2) (addErrL (msg (text "result")   k2))
-       ; unless (isMultiplicityTy kw) (addErrL (msg (text "multiplicity") kw)) }
+  = do { unless (isTYPEorCONSTRAINT k1) (report (text "argument") k1)
+       ; unless (isTYPEorCONSTRAINT k2) (report (text "result")   k2)
+       ; unless (isMultiplicityTy kw)         (report (text "multiplicity") kw) }
   where
     k1 = typeKind t1
     k2 = typeKind t2
     kw = typeKind tw
-    msg ar k
-      = vcat [ hang (text "Ill-kinded" <+> ar)
-                  2 (text "in" <+> what)
-             , what <+> text "kind:" <+> ppr k ]
+    report ar k = addErrL (vcat [ hang (text "Ill-kinded" <+> ar)
+                                     2 (text "in" <+> what)
+                                , what <+> text "kind:" <+> ppr k ])
 
 -----------------
 lint_ty_app :: Type -> LintedKind -> [LintedType] -> LintM ()
@@ -2095,7 +2106,7 @@ that returned coercion. If we get long chains, that can be asymptotically
 inefficient, notably in
 * TransCo
 * InstCo
-* NthCo (cf #9233)
+* SelCo (cf #9233)
 * LRCo
 
 But the code is simple.  And this is only Lint.  Let's wait to see if
@@ -2164,9 +2175,9 @@ lintCoercion (GRefl r ty (MCo co))
        ; return (GRefl r ty' (MCo co')) }
 
 lintCoercion co@(TyConAppCo r tc cos)
-  | tc `hasKey` funTyConKey
-  , [_w, _rep1,_rep2,_co1,_co2] <- cos
-  = failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
+  | Just {} <- tyConAppFunCo_maybe r tc cos
+  = failWithL (hang (text "Saturated application of" <+> quotes (ppr tc))
+                  2 (ppr co))
     -- All saturated TyConAppCos should be FunCos
 
   | Just {} <- synTyConDefn_maybe tc
@@ -2232,24 +2243,33 @@ lintCoercion co@(ForAllCo tcv kind_co body_co)
 
        ; return (ForAllCo tcv' kind_co' body_co') } }
 
-lintCoercion co@(FunCo r cow co1 co2)
+lintCoercion co@(FunCo { fco_role = r, fco_afl = afl, fco_afr = afr
+                       , fco_mult = cow, fco_arg = co1, fco_res = co2 })
   = do { co1' <- lintCoercion co1
        ; co2' <- lintCoercion co2
        ; cow' <- lintCoercion cow
        ; let Pair lt1 rt1 = coercionKind co1
              Pair lt2 rt2 = coercionKind co2
              Pair ltw rtw = coercionKind cow
-       ; lintArrow (text "coercion" <+> quotes (ppr co)) lt1 lt2 ltw
-       ; lintArrow (text "coercion" <+> quotes (ppr co)) rt1 rt2 rtw
+       ; lintL (afl == chooseFunTyFlag lt1 lt2) (bad_co_msg "afl")
+       ; lintL (afr == chooseFunTyFlag rt1 rt2) (bad_co_msg "afr")
+       ; lintArrow (bad_co_msg "arrowl") lt1 lt2 ltw
+       ; lintArrow (bad_co_msg "arrowr") rt1 rt2 rtw
        ; lintRole co1 r (coercionRole co1)
        ; lintRole co2 r (coercionRole co2)
-       ; ensureEqTys (typeKind ltw) multiplicityTy (text "coercion" <> quotes (ppr co))
-       ; ensureEqTys (typeKind rtw) multiplicityTy (text "coercion" <> quotes (ppr co))
+       ; ensureEqTys (typeKind ltw) multiplicityTy (bad_co_msg "mult-l")
+       ; ensureEqTys (typeKind rtw) multiplicityTy (bad_co_msg "mult-r")
        ; let expected_mult_role = case r of
                                     Phantom -> Phantom
                                     _ -> Nominal
        ; lintRole cow expected_mult_role (coercionRole cow)
-       ; return (FunCo r cow' co1' co2') }
+       ; return (co { fco_mult = cow', fco_arg = co1', fco_res = co2' }) }
+  where
+    bad_co_msg s = hang (text "Bad coercion" <+> parens (text s))
+                      2 (vcat [ text "afl:" <+> ppr afl
+                              , text "afr:" <+> ppr afr
+                              , text "arg_co:" <+> ppr co1
+                              , text "res_co:" <+> ppr co2 ])
 
 -- See Note [Bad unsafe coercion]
 lintCoercion co@(UnivCo prov r ty1 ty2)
@@ -2259,8 +2279,8 @@ lintCoercion co@(UnivCo prov r ty1 ty2)
              k2 = typeKind ty2'
        ; prov' <- lint_prov k1 k2 prov
 
-       ; when (r /= Phantom && classifiesTypeWithValues k1
-                            && classifiesTypeWithValues k2)
+       ; when (r /= Phantom && isTYPEorCONSTRAINT k1
+                            && isTYPEorCONSTRAINT k2)
               (checkTypes ty1 ty2)
 
        ; return (UnivCo prov' r ty1' ty2') }
@@ -2353,32 +2373,39 @@ lintCoercion co@(TransCo co1 co2)
        ; lintRole co (coercionRole co1) (coercionRole co2)
        ; return (TransCo co1' co2') }
 
-lintCoercion the_co@(NthCo r0 n co)
+lintCoercion the_co@(SelCo cs co)
   = do { co' <- lintCoercion co
-       ; let (Pair s t, r) = coercionKindRole co'
-       ; case (splitForAllTyCoVar_maybe s, splitForAllTyCoVar_maybe t) of
-         { (Just _, Just _)
-             -- works for both tyvar and covar
-             | n == 0
-             ,  (isForAllTy_ty s && isForAllTy_ty t)
+       ; let (Pair s t, co_role) = coercionKindRole co'
+
+       ; if -- forall (both TyVar and CoVar)
+            | Just _ <- splitForAllTyCoVar_maybe s
+            , Just _ <- splitForAllTyCoVar_maybe t
+            , SelForAll <- cs
+            ,   (isForAllTy_ty s && isForAllTy_ty t)
              || (isForAllTy_co s && isForAllTy_co t)
-             -> do { lintRole the_co Nominal r0
-                   ; return (NthCo r0 n co') }
-
-         ; _ -> case (splitTyConApp_maybe s, splitTyConApp_maybe t) of
-         { (Just (tc_s, tys_s), Just (tc_t, tys_t))
-             | tc_s == tc_t
-             , isInjectiveTyCon tc_s r
-                 -- see Note [NthCo and newtypes] in GHC.Core.TyCo.Rep
-             , tys_s `equalLength` tys_t
-             , tys_s `lengthExceeds` n
-             -> do { lintRole the_co tr r0
-                   ; return (NthCo r0 n co') }
-                where
-                  tr = nthRole r tc_s n
-
-         ; _ -> failWithL (hang (text "Bad getNth:")
-                              2 (ppr the_co $$ ppr s $$ ppr t)) }}}
+            -> return (SelCo cs co')
+
+            -- function
+            | isFunTy s
+            , isFunTy t
+            , SelFun {} <- cs
+            -> return (SelCo cs co')
+
+            -- TyCon
+            | Just (tc_s, tys_s) <- splitTyConApp_maybe s
+            , Just (tc_t, tys_t) <- splitTyConApp_maybe t
+            , tc_s == tc_t
+            , SelTyCon n r0 <- cs
+            , isInjectiveTyCon tc_s co_role
+                -- see Note [SelCo and newtypes] in GHC.Core.TyCo.Rep
+            , tys_s `equalLength` tys_t
+            , tys_s `lengthExceeds` n
+            -> do { lintRole the_co (tyConRole co_role tc_s n) r0
+                  ; return (SelCo cs co') }
+
+            | otherwise
+            -> failWithL (hang (text "Bad SelCo:")
+                             2 (ppr the_co $$ ppr s $$ ppr t)) }
 
 lintCoercion the_co@(LRCo lr co)
   = do { co' <- lintCoercion co
@@ -2586,10 +2613,14 @@ lint_branch ax_tc (CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
        ; rhs' <- lintType rhs
        ; let lhs_kind = typeKind lhs'
              rhs_kind = typeKind rhs'
-       ; lintL (lhs_kind `eqType` rhs_kind) $
+       ; lintL (not (lhs_kind `typesAreApart` rhs_kind)) $
          hang (text "Inhomogeneous axiom")
             2 (text "lhs:" <+> ppr lhs <+> dcolon <+> ppr lhs_kind $$
                text "rhs:" <+> ppr rhs <+> dcolon <+> ppr rhs_kind) }
+         -- Type and Constraint are not Apart, so this test allows
+         -- the newtype axiom for a single-method class.  Indeed the
+         -- whole reason Type and Constraint are not Apart is to allow
+         -- such axioms!
 
 -- these checks do not apply to newtype axioms
 lint_family_branch :: TyCon -> CoAxBranch -> LintM ()
@@ -3125,7 +3156,7 @@ varCallSiteUsage :: Id -> LintM UsageEnv
 varCallSiteUsage id =
   do m <- getUEAliases
      return $ case lookupNameEnv m (getName id) of
-         Nothing -> unitUE id One
+         Nothing    -> unitUE id OneTy
          Just id_ue -> id_ue
 
 ensureEqTys :: LintedType -> LintedType -> SDoc -> LintM ()
@@ -3136,7 +3167,7 @@ ensureEqTys ty1 ty2 msg = lintL (ty1 `eqType` ty2) msg
 
 ensureSubUsage :: Usage -> Mult -> SDoc -> LintM ()
 ensureSubUsage Bottom     _              _ = return ()
-ensureSubUsage Zero       described_mult err_msg = ensureSubMult Many described_mult err_msg
+ensureSubUsage Zero       described_mult err_msg = ensureSubMult ManyTy described_mult err_msg
 ensureSubUsage (MUsage m) described_mult err_msg = ensureSubMult m described_mult err_msg
 
 ensureSubMult :: Mult -> Mult -> SDoc -> LintM ()

compiler/GHC/Core/Make.hs

-
-
 {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}
 
 -- | Handy functions for creating much Core syntax
@@ -25,27 +23,22 @@ module GHC.Core.Make (
         FloatBind(..), wrapFloat, wrapFloats, floatBindings,
 
         -- * Constructing small tuples
-        mkCoreVarTupTy, mkCoreTup, mkCoreUbxTup, mkCoreUbxSum,
+        mkCoreVarTupTy, mkCoreTup, mkCoreUnboxedTuple, mkCoreUbxSum,
         mkCoreTupBoxity, unitExpr,
 
         -- * Constructing big tuples
-        mkBigCoreVarTup, mkBigCoreVarTup1,
+        mkChunkified, chunkify,
+        mkBigCoreVarTup, mkBigCoreVarTupSolo,
         mkBigCoreVarTupTy, mkBigCoreTupTy,
         mkBigCoreTup,
 
-        -- * Deconstructing small tuples
-        mkSmallTupleSelector, mkSmallTupleCase,
-
-        -- * Deconstructing big tuples
-        mkTupleSelector, mkTupleSelector1, mkTupleCase,
+          -- * Deconstructing big tuples
+        mkBigTupleSelector, mkBigTupleSelectorSolo, mkBigTupleCase,
 
         -- * Constructing list expressions
         mkNilExpr, mkConsExpr, mkListExpr,
         mkFoldrExpr, mkBuildExpr,
 
-        -- * Constructing non empty lists
-        mkNonEmptyListExpr,
-
         -- * Constructing Maybe expressions
         mkNothingExpr, mkJustExpr,
 
@@ -53,7 +46,7 @@ module GHC.Core.Make (
         mkRuntimeErrorApp, mkImpossibleExpr, mkAbsentErrorApp, errorIds,
         rEC_CON_ERROR_ID, rUNTIME_ERROR_ID,
         nON_EXHAUSTIVE_GUARDS_ERROR_ID, nO_METHOD_BINDING_ERROR_ID,
-        pAT_ERROR_ID, rEC_SEL_ERROR_ID, aBSENT_ERROR_ID,
+        pAT_ERROR_ID, rEC_SEL_ERROR_ID,
         tYPE_ERROR_ID, aBSENT_SUM_FIELD_ERROR_ID
     ) where
 
@@ -61,7 +54,7 @@ import GHC.Prelude
 import GHC.Platform
 
 import GHC.Types.Id
-import GHC.Types.Var  ( EvVar, setTyVarUnique )
+import GHC.Types.Var  ( EvVar, setTyVarUnique, visArgConstraintLike )
 import GHC.Types.TyThing
 import GHC.Types.Id.Info
 import GHC.Types.Cpr
@@ -73,12 +66,11 @@ import GHC.Types.Unique.Supply
 import GHC.Core
 import GHC.Core.Utils ( exprType, mkSingleAltCase, bindNonRec )
 import GHC.Core.Type
+import GHC.Core.TyCo.Compare( eqType )
 import GHC.Core.Coercion ( isCoVar )
 import GHC.Core.DataCon  ( DataCon, dataConWorkId )
 import GHC.Core.Multiplicity
 
-import GHC.Hs.Utils      ( mkChunkified, chunkify )
-
 import GHC.Builtin.Types
 import GHC.Builtin.Names
 import GHC.Builtin.Types.Prim
@@ -88,6 +80,7 @@ import GHC.Utils.Misc
 import GHC.Utils.Panic
 import GHC.Utils.Panic.Plain
 
+import GHC.Settings.Constants( mAX_TUPLE_SIZE )
 import GHC.Data.FastString
 
 import Data.List        ( partition )
@@ -171,9 +164,7 @@ mkCoreAppTyped _ (fun, fun_ty) (Coercion co)
   = (App fun (Coercion co), funResultTy fun_ty)
 mkCoreAppTyped d (fun, fun_ty) arg
   = assertPpr (isFunTy fun_ty) (ppr fun $$ ppr arg $$ d)
-    (App fun arg, res_ty)
-  where
-    (_mult, _arg_ty, res_ty) = splitFunTy fun_ty
+    (App fun arg, funResultTy fun_ty)
 
 {- *********************************************************************
 *                                                                      *
@@ -182,7 +173,7 @@ mkCoreAppTyped d (fun, fun_ty) arg
 ********************************************************************* -}
 
 mkWildEvBinder :: PredType -> EvVar
-mkWildEvBinder pred = mkWildValBinder Many pred
+mkWildEvBinder pred = mkWildValBinder ManyTy pred
 
 -- | Make a /wildcard binder/. This is typically used when you need a binder
 -- that you expect to use only at a *binding* site.  Do not use it at
@@ -221,7 +212,7 @@ castBottomExpr :: CoreExpr -> Type -> CoreExpr
 -- See Note [Empty case alternatives] in GHC.Core
 castBottomExpr e res_ty
   | e_ty `eqType` res_ty = e
-  | otherwise            = Case e (mkWildValBinder One e_ty) res_ty []
+  | otherwise            = Case e (mkWildValBinder OneTy e_ty) res_ty []
   where
     e_ty = exprType e
 
@@ -238,9 +229,9 @@ mkLitRubbish ty
   | isCoVarType ty
   = Nothing   -- Satisfy INVARIANT 2
   | otherwise
-  = Just (Lit (LitRubbish rep) `mkTyApps` [ty])
+  = Just (Lit (LitRubbish torc rep) `mkTyApps` [ty])
   where
-    rep  = getRuntimeRep ty
+    Just (torc, rep) = sORTKind_maybe (typeKind ty)
 
 {-
 ************************************************************************
@@ -335,22 +326,12 @@ mkStringExprFSWith ids str
 {-
 ************************************************************************
 *                                                                      *
-\subsection{Tuple constructors}
+     Creating tuples and their types for Core expressions
 *                                                                      *
 ************************************************************************
 -}
 
-{-
-Creating tuples and their types for Core expressions
-
-@mkBigCoreVarTup@ builds a tuple; the inverse to @mkTupleSelector@.
-
-* If it has only one element, it is the identity function.
-
-* If there are more elements than a big tuple can have, it nests
-  the tuples.
-
-Note [Flattening one-tuples]
+{- Note [Flattening one-tuples]
 ~~~~~~~~~~~~~~~~~~~~~~~~~~~~
 This family of functions creates a tuple of variables/expressions/types.
   mkCoreTup [e1,e2,e3] = (e1,e2,e3)
@@ -361,8 +342,8 @@ We could do one of two things:
     mkCoreTup [e1] = e1
 
 * Build a one-tuple (see Note [One-tuples] in GHC.Builtin.Types)
-    mkCoreTup1 [e1] = Solo e1
-  We use a suffix "1" to indicate this.
+    mkCoreTupSolo [e1] = Solo e1
+  We use a suffix "Solo" to indicate this.
 
 Usually we want the former, but occasionally the latter.
 
@@ -380,41 +361,46 @@ This arose from discussions in #16881.
 One-tuples that arise internally depend on the circumstance; often flattening
 is a good idea. Decisions are made on a case-by-case basis.
 
+'mkCoreBoxedTuple` and `mkBigCoreVarTupSolo` build tuples without flattening.
 -}
 
--- | Build the type of a small tuple that holds the specified variables
--- One-tuples are flattened; see Note [Flattening one-tuples]
-mkCoreVarTupTy :: [Id] -> Type
-mkCoreVarTupTy ids = mkBoxedTupleTy (map idType ids)
-
--- | Build a small tuple holding the specified expressions
--- One-tuples are flattened; see Note [Flattening one-tuples]
-mkCoreTup :: [CoreExpr] -> CoreExpr
-mkCoreTup [c] = c
-mkCoreTup cs  = mkCoreTup1 cs   -- non-1-tuples are uniform
-
 -- | Build a small tuple holding the specified expressions
 -- One-tuples are *not* flattened; see Note [Flattening one-tuples]
 -- See also Note [Don't flatten tuples from HsSyn]
-mkCoreTup1 :: [CoreExpr] -> CoreExpr
-mkCoreTup1 cs = mkCoreConApps (tupleDataCon Boxed (length cs))
-                              (map (Type . exprType) cs ++ cs)
+-- Arguments must have kind Type
+mkCoreBoxedTuple :: HasDebugCallStack => [CoreExpr] -> CoreExpr
+mkCoreBoxedTuple cs
+  = assertPpr (all (tcIsLiftedTypeKind . typeKind . exprType) cs) (ppr cs)
+    mkCoreConApps (tupleDataCon Boxed (length cs))
+                  (map (Type . exprType) cs ++ cs)
+
 
--- | Build a small unboxed tuple holding the specified expressions,
--- with the given types. The types must be the types of the expressions.
+-- | Build a small unboxed tuple holding the specified expressions.
 -- Do not include the RuntimeRep specifiers; this function calculates them
 -- for you.
 -- Does /not/ flatten one-tuples; see Note [Flattening one-tuples]
-mkCoreUbxTup :: [Type] -> [CoreExpr] -> CoreExpr
-mkCoreUbxTup tys exps
-  = assert (tys `equalLength` exps) $
-    mkCoreConApps (tupleDataCon Unboxed (length tys))
-             (map (Type . getRuntimeRep) tys ++ map Type tys ++ exps)
+mkCoreUnboxedTuple :: [CoreExpr] -> CoreExpr
+mkCoreUnboxedTuple exps
+  = mkCoreConApps (tupleDataCon Unboxed (length tys))
+                  (map (Type . getRuntimeRep) tys ++ map Type tys ++ exps)
+  where
+    tys = map exprType exps
 
 -- | Make a core tuple of the given boxity; don't flatten 1-tuples
 mkCoreTupBoxity :: Boxity -> [CoreExpr] -> CoreExpr
-mkCoreTupBoxity Boxed   exps = mkCoreTup1 exps
-mkCoreTupBoxity Unboxed exps = mkCoreUbxTup (map exprType exps) exps
+mkCoreTupBoxity Boxed   exps = mkCoreBoxedTuple   exps
+mkCoreTupBoxity Unboxed exps = mkCoreUnboxedTuple exps
+
+-- | Build the type of a small tuple that holds the specified variables
+-- One-tuples are flattened; see Note [Flattening one-tuples]
+mkCoreVarTupTy :: [Id] -> Type
+mkCoreVarTupTy ids = mkBoxedTupleTy (map idType ids)
+
+-- | Build a small tuple holding the specified expressions
+-- One-tuples are flattened; see Note [Flattening one-tuples]
+mkCoreTup :: [CoreExpr] -> CoreExpr
+mkCoreTup [c] = c
+mkCoreTup cs  = mkCoreBoxedTuple cs   -- non-1-tuples are uniform
 
 -- | Build an unboxed sum.
 --
@@ -428,37 +414,153 @@ mkCoreUbxSum arity alt tys exp
                    ++ map Type tys
                    ++ [exp])
 
+{- Note [Big tuples]
+~~~~~~~~~~~~~~~~~~~~
+"Big" tuples (`mkBigCoreTup` and friends) are more general than "small"
+ones (`mkCoreTup` and friends) in two ways.
+
+1. GHCs built-in tuples can only go up to 'mAX_TUPLE_SIZE' in arity, but
+   we might conceivably want to build such a massive tuple as part of the
+   output of a desugaring stage (notably that for list comprehensions).
+
+   `mkBigCoreTup` encodes such big tuples by creating and pattern
+   matching on /nested/ small tuples that are directly expressible by
+   GHC.
+
+   Nesting policy: it's better to have a 2-tuple of 10-tuples (3 objects)
+   than a 10-tuple of 2-tuples (11 objects), so we want the leaves of any
+   construction to be big.
+
+2. When desugaring arrows we gather up a tuple of free variables, which
+   may include dictionaries (of kind Constraint) and unboxed values.
+
+   These can't live in a tuple. `mkBigCoreTup` encodes such tuples by
+   boxing up the offending arguments: see Note [Boxing constructors]
+   in GHC.Builtin.Types.
+
+If you just use the 'mkBigCoreTup', 'mkBigCoreVarTupTy', 'mkBigTupleSelector'
+and 'mkBigTupleCase' functions to do all your work with tuples you should be
+fine, and not have to worry about the arity limitation, or kind limitation at
+all.
+
+The "big" tuple operations flatten 1-tuples just like "small" tuples.
+But see Note [Don't flatten tuples from HsSyn]
+-}
+
+mkBigCoreVarTupSolo :: [Id] -> CoreExpr
+-- Same as mkBigCoreVarTup, but:
+--   - one-tuples are not flattened
+--     see Note [Flattening one-tuples]
+--   - arguments should have kind Type
+mkBigCoreVarTupSolo [id] = mkCoreBoxedTuple [Var id]
+mkBigCoreVarTupSolo ids  = mkChunkified mkCoreTup (map Var ids)
+
 -- | Build a big tuple holding the specified variables
 -- One-tuples are flattened; see Note [Flattening one-tuples]
+-- Arguments don't have to have kind Type
 mkBigCoreVarTup :: [Id] -> CoreExpr
 mkBigCoreVarTup ids = mkBigCoreTup (map Var ids)
 
-mkBigCoreVarTup1 :: [Id] -> CoreExpr
--- Same as mkBigCoreVarTup, but one-tuples are NOT flattened
---                          see Note [Flattening one-tuples]
-mkBigCoreVarTup1 [id] = mkCoreConApps (tupleDataCon Boxed 1)
-                                      [Type (idType id), Var id]
-mkBigCoreVarTup1 ids  = mkBigCoreTup (map Var ids)
+-- | Build a "big" tuple holding the specified expressions
+-- One-tuples are flattened; see Note [Flattening one-tuples]
+-- Arguments don't have to have kind Type; ones that do not are boxed
+-- This function crashes (in wrapBox) if given a non-Type
+-- argument that it doesn't know how to box.
+mkBigCoreTup :: [CoreExpr] -> CoreExpr
+mkBigCoreTup exprs = mkChunkified mkCoreTup (map wrapBox exprs)
 
 -- | Build the type of a big tuple that holds the specified variables
 -- One-tuples are flattened; see Note [Flattening one-tuples]
 mkBigCoreVarTupTy :: [Id] -> Type
 mkBigCoreVarTupTy ids = mkBigCoreTupTy (map idType ids)
 
--- | Build a big tuple holding the specified expressions
--- One-tuples are flattened; see Note [Flattening one-tuples]
-mkBigCoreTup :: [CoreExpr] -> CoreExpr
-mkBigCoreTup = mkChunkified mkCoreTup
-
 -- | Build the type of a big tuple that holds the specified type of thing
 -- One-tuples are flattened; see Note [Flattening one-tuples]
 mkBigCoreTupTy :: [Type] -> Type
-mkBigCoreTupTy = mkChunkified mkBoxedTupleTy
+mkBigCoreTupTy tys = mkChunkified mkBoxedTupleTy $
+                     map boxTy tys
 
 -- | The unit expression
 unitExpr :: CoreExpr
 unitExpr = Var unitDataConId
 
+--------------------------------------------------------------
+wrapBox :: CoreExpr -> CoreExpr
+-- ^ If (e :: ty) and (ty :: Type), wrapBox is a no-op
+-- But if (ty :: ki), and ki is not Type, wrapBox returns (K @ty e)
+--     which has kind Type
+-- where K is the boxing data constructor for ki
+-- See Note [Boxing constructors] in GHC.Builtin.Types
+-- Panics if there /is/ no boxing data con
+wrapBox e
+  = case boxingDataCon e_ty of
+      BI_NoBoxNeeded                       -> e
+      BI_Box { bi_inst_con = boxing_expr } -> App boxing_expr e
+      BI_NoBoxAvailable -> pprPanic "wrapBox" (ppr e $$ ppr (exprType e))
+                           -- We should do better than panicing: #22336
+  where
+    e_ty = exprType e
+
+boxTy :: Type -> Type
+-- ^ `boxTy ty` is the boxed version of `ty`. That is,
+-- if `e :: ty`, then `wrapBox e :: boxTy ty`.
+-- Note that if `ty :: Type`, `boxTy ty` just returns `ty`.
+-- Panics if it is not possible to box `ty`, in line with the behaviour of `wrapBox`
+-- See Note [Boxing constructors] in GHC.Builtin.Types
+boxTy ty
+  = case boxingDataCon ty of
+      BI_NoBoxNeeded -> ty
+      BI_Box { bi_boxed_type = box_ty } -> box_ty
+      BI_NoBoxAvailable -> pprPanic "boxTy" (ppr ty)
+                           -- We should do better than panicing: #22336
+
+unwrapBox :: UniqSupply -> Id -> CoreExpr
+                 -> (UniqSupply, Id, CoreExpr)
+-- If v's type required boxing (i.e it is unlifted or a constraint)
+-- then (unwrapBox us v body) returns
+--          (case box_v of MkDict v -> body)
+--          together with box_v
+--      where box_v is a fresh variable
+-- Otherwise unwrapBox is a no-op
+-- Panics if no box is available
+unwrapBox us var body
+  = case boxingDataCon var_ty of
+      BI_NoBoxNeeded    -> (us, var, body)
+      BI_NoBoxAvailable -> pprPanic "unwrapBox" (ppr var $$ ppr var_ty)
+                           -- We should do better than panicing: #22336
+      BI_Box { bi_data_con = box_con, bi_boxed_type = box_ty }
+         -> (us', var', body')
+         where
+           var'  = mkSysLocal (fsLit "uc") uniq ManyTy box_ty
+           body' = Case (Var var') var' (exprType body)
+                        [Alt (DataAlt box_con) [var] body]
+  where
+    var_ty      = idType var
+    (uniq, us') = takeUniqFromSupply us
+
+-- | Lifts a \"small\" constructor into a \"big\" constructor by recursive decomposition
+mkChunkified :: ([a] -> a)      -- ^ \"Small\" constructor function, of maximum input arity 'mAX_TUPLE_SIZE'
+             -> [a]             -- ^ Possible \"big\" list of things to construct from
+             -> a               -- ^ Constructed thing made possible by recursive decomposition
+mkChunkified small_tuple as = mk_big_tuple (chunkify as)
+  where
+        -- Each sub-list is short enough to fit in a tuple
+    mk_big_tuple [as] = small_tuple as
+    mk_big_tuple as_s = mk_big_tuple (chunkify (map small_tuple as_s))
+
+chunkify :: [a] -> [[a]]
+-- ^ Split a list into lists that are small enough to have a corresponding
+-- tuple arity. The sub-lists of the result all have length <= 'mAX_TUPLE_SIZE'
+-- But there may be more than 'mAX_TUPLE_SIZE' sub-lists
+chunkify xs
+  | n_xs <= mAX_TUPLE_SIZE = [xs]
+  | otherwise              = split xs
+  where
+    n_xs     = length xs
+    split [] = []
+    split xs = take mAX_TUPLE_SIZE xs : split (drop mAX_TUPLE_SIZE xs)
+
+
 {-
 ************************************************************************
 *                                                                      *
@@ -479,16 +581,16 @@ unitExpr = Var unitDataConId
 -- If necessary, we pattern match on a \"big\" tuple.
 --
 -- A tuple selector is not linear in its argument. Consequently, the case
--- expression built by `mkTupleSelector` must consume its scrutinee 'Many'
+-- expression built by `mkBigTupleSelector` must consume its scrutinee 'Many'
 -- times. And all the argument variables must have multiplicity 'Many'.
-mkTupleSelector, mkTupleSelector1
+mkBigTupleSelector, mkBigTupleSelectorSolo
     :: [Id]         -- ^ The 'Id's to pattern match the tuple against
     -> Id           -- ^ The 'Id' to select
     -> Id           -- ^ A variable of the same type as the scrutinee
     -> CoreExpr     -- ^ Scrutinee
     -> CoreExpr     -- ^ Selector expression
 
--- mkTupleSelector [a,b,c,d] b v e
+-- mkBigTupleSelector [a,b,c,d] b v e
 --          = case e of v {
 --                (p,q) -> case p of p {
 --                           (a,b) -> b }}
@@ -499,7 +601,7 @@ mkTupleSelector, mkTupleSelector1
 --        case (case e of v
 --                (p,q) -> p) of p
 --          (a,b) -> b
-mkTupleSelector vars the_var scrut_var scrut
+mkBigTupleSelector vars the_var scrut_var scrut
   = mk_tup_sel (chunkify vars) the_var
   where
     mk_tup_sel [vars] the_var = mkSmallTupleSelector vars the_var scrut_var scrut
@@ -508,18 +610,18 @@ mkTupleSelector vars the_var scrut_var scrut
         where
           tpl_tys = [mkBoxedTupleTy (map idType gp) | gp <- vars_s]
           tpl_vs  = mkTemplateLocals tpl_tys
-          [(tpl_v, group)] = [(tpl,gp) | (tpl,gp) <- zipEqual "mkTupleSelector" tpl_vs vars_s,
+          [(tpl_v, group)] = [(tpl,gp) | (tpl,gp) <- zipEqual "mkBigTupleSelector" tpl_vs vars_s,
                                          the_var `elem` gp ]
--- ^ 'mkTupleSelector1' is like 'mkTupleSelector'
+-- ^ 'mkBigTupleSelectorSolo' is like 'mkBigTupleSelector'
 -- but one-tuples are NOT flattened (see Note [Flattening one-tuples])
-mkTupleSelector1 vars the_var scrut_var scrut
+mkBigTupleSelectorSolo vars the_var scrut_var scrut
   | [_] <- vars
   = mkSmallTupleSelector1 vars the_var scrut_var scrut
   | otherwise
-  = mkTupleSelector vars the_var scrut_var scrut
+  = mkBigTupleSelector vars the_var scrut_var scrut
 
--- | Like 'mkTupleSelector' but for tuples that are guaranteed
--- never to be \"big\".
+-- | `mkSmallTupleSelector` is like 'mkBigTupleSelector', but for tuples that
+-- are guaranteed never to be "big".  Also does not unwrap boxed types.
 --
 -- > mkSmallTupleSelector [x] x v e = [| e |]
 -- > mkSmallTupleSelector [x,y,z] x v e = [| case e of v { (x,y,z) -> x } |]
@@ -542,45 +644,71 @@ mkSmallTupleSelector1 vars the_var scrut_var scrut
     Case scrut scrut_var (idType the_var)
          [Alt (DataAlt (tupleDataCon Boxed (length vars))) vars (Var the_var)]
 
--- | A generalization of 'mkTupleSelector', allowing the body
+-- | A generalization of 'mkBigTupleSelector', allowing the body
 -- of the case to be an arbitrary expression.
 --
 -- To avoid shadowing, we use uniques to invent new variables.
 --
--- If necessary we pattern match on a \"big\" tuple.
-mkTupleCase :: UniqSupply       -- ^ For inventing names of intermediate variables
-            -> [Id]             -- ^ The tuple identifiers to pattern match on
-            -> CoreExpr         -- ^ Body of the case
-            -> Id               -- ^ A variable of the same type as the scrutinee
-            -> CoreExpr         -- ^ Scrutinee
-            -> CoreExpr
+-- If necessary we pattern match on a "big" tuple.
+mkBigTupleCase :: UniqSupply       -- ^ For inventing names of intermediate variables
+               -> [Id]             -- ^ The tuple identifiers to pattern match on;
+                                   --   Bring these into scope in the body
+               -> CoreExpr         -- ^ Body of the case
+               -> CoreExpr         -- ^ Scrutinee
+               -> CoreExpr
 -- ToDo: eliminate cases where none of the variables are needed.
 --
---         mkTupleCase uniqs [a,b,c,d] body v e
+--         mkBigTupleCase uniqs [a,b,c,d] body v e
 --           = case e of v { (p,q) ->
 --             case p of p { (a,b) ->
 --             case q of q { (c,d) ->
 --             body }}}
-mkTupleCase uniqs vars body scrut_var scrut
-  = mk_tuple_case uniqs (chunkify vars) body
+mkBigTupleCase us vars body scrut
+  = mk_tuple_case wrapped_us (chunkify wrapped_vars) wrapped_body
   where
+    (wrapped_us, wrapped_vars, wrapped_body) = foldr unwrap (us,[],body) vars
+
+    scrut_ty = exprType scrut
+
+    unwrap var (us,vars,body)
+      = (us', var':vars, body')
+      where
+        (us', var', body') = unwrapBox us var body
+
+    mk_tuple_case :: UniqSupply -> [[Id]] -> CoreExpr -> CoreExpr
+    -- mk_tuple_case [[a1..an], [b1..bm], ...] body
+    --    case scrut of (p,q, ...) ->
+    --    case p of (a1,..an) ->
+    --    case q of (b1,..bm) ->
+    --    ... -> body
     -- This is the case where don't need any nesting
-    mk_tuple_case _ [vars] body
+    mk_tuple_case us [vars] body
       = mkSmallTupleCase vars body scrut_var scrut
+      where
+        scrut_var = case scrut of
+                       Var v -> v
+                       _ -> snd (new_var us scrut_ty)
 
-    -- This is the case where we must make nest tuples at least once
+    -- This is the case where we must nest tuples at least once
     mk_tuple_case us vars_s body
-      = let (us', vars', body') = foldr one_tuple_case (us, [], body) vars_s
-            in mk_tuple_case us' (chunkify vars') body'
+      = mk_tuple_case us' (chunkify vars') body'
+      where
+        (us', vars', body') = foldr one_tuple_case (us, [], body) vars_s
 
     one_tuple_case chunk_vars (us, vs, body)
-      = let (uniq, us') = takeUniqFromSupply us
-            scrut_var = mkSysLocal (fsLit "ds") uniq Many
-              (mkBoxedTupleTy (map idType chunk_vars))
-            body' = mkSmallTupleCase chunk_vars body scrut_var (Var scrut_var)
-        in (us', scrut_var:vs, body')
-
--- | As 'mkTupleCase', but for a tuple that is small enough to be guaranteed
+      = (us', scrut_var:vs, body')
+      where
+        tup_ty           = mkBoxedTupleTy (map idType chunk_vars)
+        (us', scrut_var) = new_var us tup_ty
+        body' = mkSmallTupleCase chunk_vars body scrut_var (Var scrut_var)
+
+    new_var :: UniqSupply -> Type -> (UniqSupply, Id)
+    new_var us ty = (us', id)
+       where
+         (uniq, us') = takeUniqFromSupply us
+         id = mkSysLocal (fsLit "ds") uniq ManyTy ty
+
+-- | As 'mkBigTupleCase', but for a tuple that is small enough to be guaranteed
 -- not to need nesting.
 mkSmallTupleCase
         :: [Id]         -- ^ The tuple args
@@ -592,7 +720,6 @@ mkSmallTupleCase
 mkSmallTupleCase [var] body _scrut_var scrut
   = bindNonRec var scrut body
 mkSmallTupleCase vars body scrut_var scrut
--- One branch no refinement?
   = Case scrut scrut_var (exprType body)
          [Alt (DataAlt (tupleDataCon Boxed (length vars))) vars body]
 
@@ -655,9 +782,6 @@ mkConsExpr ty hd tl = mkCoreConApps consDataCon [Type ty, hd, tl]
 mkListExpr :: Type -> [CoreExpr] -> CoreExpr
 mkListExpr ty xs = foldr (mkConsExpr ty) (mkNilExpr ty) xs
 
-mkNonEmptyListExpr :: Type -> CoreExpr -> [CoreExpr] -> CoreExpr
-mkNonEmptyListExpr ty x xs = mkCoreConApps nonEmptyDataCon [Type ty, x, mkListExpr ty xs]
-
 -- | Make a fully applied 'foldr' expression
 mkFoldrExpr :: MonadThings m
             => Type             -- ^ Element type of the list
@@ -685,7 +809,7 @@ mkBuildExpr elt_ty mk_build_inside = do
     n_tyvar <- newTyVar alphaTyVar
     let n_ty = mkTyVarTy n_tyvar
         c_ty = mkVisFunTysMany [elt_ty, n_ty] n_ty
-    [c, n] <- sequence [mkSysLocalM (fsLit "c") Many c_ty, mkSysLocalM (fsLit "n") Many n_ty]
+    [c, n] <- sequence [mkSysLocalM (fsLit "c") ManyTy c_ty, mkSysLocalM (fsLit "n") ManyTy n_ty]
 
     build_inside <- mk_build_inside (c, c_ty) (n, n_ty)
 
@@ -766,12 +890,12 @@ errorIds
       pAT_ERROR_ID,
       rEC_CON_ERROR_ID,
       rEC_SEL_ERROR_ID,
-      aBSENT_ERROR_ID,
+      aBSENT_ERROR_ID, aBSENT_CONSTRAINT_ERROR_ID,
       aBSENT_SUM_FIELD_ERROR_ID,
       tYPE_ERROR_ID   -- Used with Opt_DeferTypeErrors, see #10284
       ]
 
-recSelErrorName, runtimeErrorName, absentErrorName :: Name
+recSelErrorName, runtimeErrorName :: Name
 recConErrorName, patErrorName :: Name
 nonExhaustiveGuardsErrorName, noMethodBindingErrorName :: Name
 typeErrorName :: Name
@@ -793,7 +917,7 @@ err_nm str uniq id = mkWiredInIdName cONTROL_EXCEPTION_BASE (fsLit str) uniq id
 
 rEC_SEL_ERROR_ID, rUNTIME_ERROR_ID, rEC_CON_ERROR_ID :: Id
 pAT_ERROR_ID, nO_METHOD_BINDING_ERROR_ID, nON_EXHAUSTIVE_GUARDS_ERROR_ID :: Id
-tYPE_ERROR_ID, aBSENT_ERROR_ID, aBSENT_SUM_FIELD_ERROR_ID :: Id
+tYPE_ERROR_ID, aBSENT_SUM_FIELD_ERROR_ID :: Id
 rEC_SEL_ERROR_ID                = mkRuntimeErrorId recSelErrorName
 rUNTIME_ERROR_ID                = mkRuntimeErrorId runtimeErrorName
 rEC_CON_ERROR_ID                = mkRuntimeErrorId recConErrorName
@@ -901,13 +1025,6 @@ absentSumFieldErrorName
       absentSumFieldErrorIdKey
       aBSENT_SUM_FIELD_ERROR_ID
 
-absentErrorName
-   = mkWiredInIdName
-      gHC_PRIM_PANIC
-      (fsLit "absentError")
-      absentErrorIdKey
-      aBSENT_ERROR_ID
-
 aBSENT_SUM_FIELD_ERROR_ID = mkExceptionId absentSumFieldErrorName
 
 -- | Exception with type \"forall a. a\"
@@ -1054,19 +1171,51 @@ but that should be okay; since there's no pattern match we can't really
 be relying on anything from it.
 -}
 
-aBSENT_ERROR_ID -- See Note [aBSENT_ERROR_ID]
- = mkVanillaGlobalWithInfo absentErrorName absent_ty id_info
- where
-   absent_ty = mkSpecForAllTys [alphaTyVar] (mkVisFunTyMany addrPrimTy alphaTy)
-   -- Not runtime-rep polymorphic. aBSENT_ERROR_ID is only used for
-   -- lifted-type things; see Note [Absent fillers] in GHC.Core.Opt.WorkWrap.Utils
-   id_info = divergingIdInfo [evalDmd] -- NB: CAFFY!
+-- We need two absentError Ids:
+--   absentError           :: forall (a :: Type).       Addr# -> a
+--   absentConstraintError :: forall (a :: Constraint). Addr# -> a
+-- We don't have polymorphism over TypeOrConstraint!
+-- mkAbsentErrorApp chooses which one to use, based on the kind
 
 mkAbsentErrorApp :: Type         -- The type to instantiate 'a'
                  -> String       -- The string to print
                  -> CoreExpr
 
 mkAbsentErrorApp res_ty err_msg
-  = mkApps (Var aBSENT_ERROR_ID) [ Type res_ty, err_string ]
+  = mkApps (Var err_id) [ Type res_ty, err_string ]
   where
+    err_id | isConstraintLikeKind (typeKind res_ty) = aBSENT_CONSTRAINT_ERROR_ID
+           | otherwise                              = aBSENT_ERROR_ID
     err_string = Lit (mkLitString err_msg)
+
+absentErrorName, absentConstraintErrorName :: Name
+absentErrorName
+   = mkWiredInIdName gHC_PRIM_PANIC (fsLit "absentError")
+      absentErrorIdKey aBSENT_ERROR_ID
+
+absentConstraintErrorName
+   = mkWiredInIdName gHC_PRIM_PANIC (fsLit "absentConstraintError")
+      absentConstraintErrorIdKey aBSENT_CONSTRAINT_ERROR_ID
+
+aBSENT_ERROR_ID, aBSENT_CONSTRAINT_ERROR_ID :: Id
+
+aBSENT_ERROR_ID -- See Note [aBSENT_ERROR_ID]
+ = mkVanillaGlobalWithInfo absentErrorName absent_ty id_info
+ where
+   -- absentError :: forall (a :: Type). Addr# -> a
+   absent_ty = mkSpecForAllTys [alphaTyVar] $
+               mkVisFunTyMany addrPrimTy (mkTyVarTy alphaTyVar)
+   -- Not runtime-rep polymorphic. aBSENT_ERROR_ID is only used for
+   -- lifted-type things; see Note [Absent fillers] in GHC.Core.Opt.WorkWrap.Utils
+   id_info = divergingIdInfo [evalDmd] -- NB: CAFFY!
+
+aBSENT_CONSTRAINT_ERROR_ID -- See Note [aBSENT_ERROR_ID]
+ = mkVanillaGlobalWithInfo absentConstraintErrorName absent_ty id_info
+ where
+   -- absentConstraintError :: forall (a :: Constraint). Addr# -> a
+   absent_ty = mkSpecForAllTys [alphaConstraintTyVar] $
+               mkFunTy visArgConstraintLike ManyTy
+                       addrPrimTy (mkTyVarTy alphaConstraintTyVar)
+   id_info = divergingIdInfo [evalDmd] -- NB: CAFFY!
+
+

compiler/GHC/Core/Map/Expr.hs

@@ -150,9 +150,8 @@ instance Eq (DeBruijn CoreExpr) where
 
 eqDeBruijnExpr :: DeBruijn CoreExpr -> DeBruijn CoreExpr -> Bool
 eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
-    go (Var v1) (Var v2) = eqDeBruijnVar (D env1 v1) (D env2 v2)
+    go (Var v1) (Var v2)             = eqDeBruijnVar (D env1 v1) (D env2 v2)
     go (Lit lit1)    (Lit lit2)      = lit1 == lit2
-    -- See Note [Using tcView inside eqDeBruijnType] in GHC.Core.Map.Type
     go (Type t1)    (Type t2)        = eqDeBruijnType (D env1 t1) (D env2 t2)
     -- See Note [Alpha-equality for Coercion arguments]
     go (Coercion {}) (Coercion {}) = True
@@ -163,7 +162,6 @@ eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
       && go e1 e2
 
     go (Lam b1 e1)  (Lam b2 e2)
-          -- See Note [Using tcView inside eqDeBruijnType] in GHC.Core.Map.Type
       =  eqDeBruijnType (D env1 (varType b1)) (D env2 (varType b2))
       && D env1 (varMultMaybe b1) == D env2 (varMultMaybe b2)
       && eqDeBruijnExpr (D (extendCME env1 b1) e1) (D (extendCME env2 b2) e2)
@@ -175,9 +173,7 @@ eqDeBruijnExpr (D env1 e1) (D env2 e2) = go e1 e2 where
     go (Let (Rec ps1) e1) (Let (Rec ps2) e2)
       = equalLength ps1 ps2
       -- See Note [Alpha-equality for let-bindings]
-      && all2 (\b1 b2 -> -- See Note [Using tcView inside eqDeBruijnType] in
-                         -- GHC.Core.Map.Type
-                         eqDeBruijnType (D env1 (varType b1))
+      && all2 (\b1 b2 -> eqDeBruijnType (D env1 (varType b1))
                                         (D env2 (varType b2)))
               bs1 bs2
       && D env1' rs1 == D env2' rs2