Generalize kind of the (->) tycon

This is generalizes the kind of `(->)`, as discussed in #11714.

This involves a few things,

 * Generalizing the kind of `funTyCon`, adding two new `RuntimeRep`
binders,
  ```lang=haskell
(->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
               (a :: TYPE r1) (b :: TYPE r2).
        a -> b -> *
  ```

 * Unsaturated applications of `(->)` are expressed as explicit
`TyConApp`s

 * Saturated applications of `(->)` are expressed as `FunTy` as they are
currently

 * Saturated applications of `(->)` are expressed by a new `FunCo`
constructor in coercions

 * `splitTyConApp` needs to ensure that `FunTy`s are split to a
`TyConApp`
   of `(->)` with the appropriate `RuntimeRep` arguments

 * Teach CoreLint to check that all saturated applications of `(->)` are
represented with `FunTy`

At the moment I assume that `Constraint ~ *`, which is an annoying
source of complexity. This will
be simplified once D3023 is resolved.

Also, this introduces two known regressions,

`tcfail181`, `T10403`
=====================
Only shows the instance,

    instance Monad ((->) r) -- Defined in ‘GHC.Base’

in its error message when -fprint-potential-instances is used. This is
because its instance head now mentions 'LiftedRep which is not in scope.
I'm not entirely sure of the right way to fix this so I'm just accepting
the new output for now.

T5963 (Typeable)
================

T5963 is now broken since Data.Typeable.Internals.mkFunTy computes its
fingerprint without the RuntimeRep variables that (->) expects. This
will be fixed with the merge of D2010.

Haddock performance
===================

The `haddock.base` and `haddock.Cabal` tests regress in allocations by
about 20%. This certainly hurts, but it's also not entirely unexpected:
the size of every function type grows with this patch and Haddock has a
lot of functions in its heap.

31 files changed, 480 insertions, 115 deletions

diff --git a/compiler/coreSyn/CoreFVs.hs b/compiler/coreSyn/CoreFVs.hs
index eba64cdb56..3a90ea0f03 100644
--- a/compiler/coreSyn/CoreFVs.hs
+++ b/compiler/coreSyn/CoreFVs.hs
@@ -373,6 +373,7 @@ orphNamesOfCo (TyConAppCo _ tc cos) = unitNameSet (getName tc) `unionNameSet` or
 orphNamesOfCo (AppCo co1 co2)       = orphNamesOfCo co1 `unionNameSet` orphNamesOfCo co2
 orphNamesOfCo (ForAllCo _ kind_co co)
   = orphNamesOfCo kind_co `unionNameSet` orphNamesOfCo co
+orphNamesOfCo (FunCo _ co1 co2)     = 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
diff --git a/compiler/coreSyn/CoreLint.hs b/compiler/coreSyn/CoreLint.hs
index 053ac21d15..2f34046d6a 100644
--- a/compiler/coreSyn/CoreLint.hs
+++ b/compiler/coreSyn/CoreLint.hs
@@ -130,6 +130,12 @@ Outstanding issues:
     --   may well be happening...);
 
 
+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.
+
 Note [Linting type lets]
 ~~~~~~~~~~~~~~~~~~~~~~~~
 In the desugarer, it's very very convenient to be able to say (in effect)
@@ -1245,6 +1251,13 @@ lintType ty@(TyConApp tc tys)
   = lintType ty'   -- Expand type synonyms, so that we do not bogusly complain
                    --  about un-saturated type synonyms
 
+  -- 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].
+  | isFunTyCon tc
+  , length tys == 4
+  = failWithL (hang (text "Saturated application of (->)") 2 (ppr ty))
+
   | isTypeSynonymTyCon tc || isTypeFamilyTyCon tc
        -- Also type synonyms and type families
   , length tys < tyConArity tc
@@ -1487,14 +1500,9 @@ lintCoercion (Refl r ty)
 
 lintCoercion co@(TyConAppCo r tc cos)
   | tc `hasKey` funTyConKey
-  , [co1,co2] <- cos
-  = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
-       ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
-       ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
-       ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
-       ; lintRole co1 r r1
-       ; lintRole co2 r r2
-       ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
+  , [_rep1,_rep2,_co1,_co2] <- cos
+  = do { failWithL (text "Saturated TyConAppCo (->):" <+> ppr co)
+       } -- All saturated TyConAppCos should be FunCos
 
   | Just {} <- synTyConDefn_maybe tc
   = failWithL (text "Synonym in TyConAppCo:" <+> ppr co)
@@ -1545,6 +1553,15 @@ lintCoercion (ForAllCo tv1 kind_co co)
                    substTy subst t2
        ; return (k3, k4, tyl, tyr, r) } }
 
+lintCoercion co@(FunCo r co1 co2)
+  = do { (k1,k'1,s1,t1,r1) <- lintCoercion co1
+       ; (k2,k'2,s2,t2,r2) <- lintCoercion co2
+       ; k <- lintArrow (text "coercion" <+> quotes (ppr co)) k1 k2
+       ; k' <- lintArrow (text "coercion" <+> quotes (ppr co)) k'1 k'2
+       ; lintRole co1 r r1
+       ; lintRole co2 r r2
+       ; return (k, k', mkFunTy s1 s2, mkFunTy t1 t2, r) }
+
 lintCoercion (CoVarCo cv)
   | not (isCoVar cv)
   = failWithL (hang (text "Bad CoVarCo:" <+> ppr cv)
diff --git a/compiler/coreSyn/CoreSubst.hs b/compiler/coreSyn/CoreSubst.hs
index d669569d18..89a92f886a 100644
--- a/compiler/coreSyn/CoreSubst.hs
+++ b/compiler/coreSyn/CoreSubst.hs
@@ -1678,7 +1678,7 @@ pushCoValArg co
   = Just (mkRepReflCo arg, mkRepReflCo res)
 
   | isFunTy tyL
-  , [co1, co2] <- decomposeCo 2 co
+  , [_, _, co1, co2] <- decomposeCo 4 co
               -- If   co  :: (tyL1 -> tyL2) ~ (tyR1 -> tyR2)
               -- then co1 :: tyL1 ~ tyR1
               --      co2 :: tyL2 ~ tyR2
@@ -1702,7 +1702,7 @@ pushCoercionIntoLambda in_scope x e co
     , Pair s1s2 t1t2 <- coercionKind co
     , Just (_s1,_s2) <- splitFunTy_maybe s1s2
     , Just (t1,_t2) <- splitFunTy_maybe t1t2
-    = let [co1, co2] = decomposeCo 2 co
+    = let [_rep1, _rep2, co1, co2] = decomposeCo 4 co
           -- Should we optimize the coercions here?
           -- Otherwise they might not match too well
           x' = x `setIdType` t1
diff --git a/compiler/coreSyn/TrieMap.hs b/compiler/coreSyn/TrieMap.hs
index 4a6e2452fd..710d80d251 100644
--- a/compiler/coreSyn/TrieMap.hs
+++ b/compiler/coreSyn/TrieMap.hs
@@ -796,9 +796,9 @@ data TypeMapX a
 -- to nested AppTys. Why the last one? See Note [Equality on AppTys] in Type
 trieMapView :: Type -> Maybe Type
 trieMapView ty | Just ty' <- coreViewOneStarKind ty = Just ty'
-trieMapView (TyConApp tc tys@(_:_)) = Just $ foldl AppTy (TyConApp tc []) tys
-trieMapView (FunTy arg res)
-  = Just ((TyConApp funTyCon [] `AppTy` arg) `AppTy` res)
+trieMapView ty
+  | Just (tc, tys@(_:_)) <- splitTyConApp_maybe ty
+  = Just $ foldl AppTy (TyConApp tc []) tys
 trieMapView _ = Nothing
 
 instance TrieMap TypeMapX where
diff --git a/compiler/iface/ToIface.hs b/compiler/iface/ToIface.hs
index 37d41f4393..c0229b8e62 100644
--- a/compiler/iface/ToIface.hs
+++ b/compiler/iface/ToIface.hs
@@ -201,9 +201,9 @@ toIfaceTyLit (StrTyLit x) = IfaceStrTyLit x
 ----------------
 toIfaceCoercion :: Coercion -> IfaceCoercion
 toIfaceCoercion (Refl r ty)         = IfaceReflCo r (toIfaceType ty)
-toIfaceCoercion (TyConAppCo r tc cos)
+toIfaceCoercion co@(TyConAppCo r tc cos)
   | tc `hasKey` funTyConKey
-  , [arg,res] <- cos                = IfaceFunCo r (toIfaceCoercion arg) (toIfaceCoercion res)
+  , [_,_,_,_] <- cos                = pprPanic "toIfaceCoercion" (ppr co)
   | otherwise                       = IfaceTyConAppCo r (toIfaceTyCon tc)
                                                         (map toIfaceCoercion cos)
 toIfaceCoercion (AppCo co1 co2)     = IfaceAppCo  (toIfaceCoercion co1)
@@ -211,6 +211,8 @@ toIfaceCoercion (AppCo co1 co2)     = IfaceAppCo  (toIfaceCoercion co1)
 toIfaceCoercion (ForAllCo tv k co)  = IfaceForAllCo (toIfaceTvBndr tv)
                                                     (toIfaceCoercion k)
                                                     (toIfaceCoercion co)
+toIfaceCoercion (FunCo r co1 co2)   = IfaceFunCo r (toIfaceCoercion co1)
+                                                   (toIfaceCoercion co2)
 toIfaceCoercion (CoVarCo cv)        = IfaceCoVarCo  (toIfaceCoVar cv)
 toIfaceCoercion (AxiomInstCo con ind cos)
                                     = IfaceAxiomInstCo (coAxiomName con) ind
diff --git a/compiler/prelude/TysPrim.hs b/compiler/prelude/TysPrim.hs
index df8a380b83..cdc25e0fc6 100644
--- a/compiler/prelude/TysPrim.hs
+++ b/compiler/prelude/TysPrim.hs
@@ -24,7 +24,7 @@ module TysPrim(
         openAlphaTy, openBetaTy, openAlphaTyVar, openBetaTyVar,
 
         -- Kind constructors...
-        tYPETyConName,
+        tYPETyCon, tYPETyConName,
 
         -- Kinds
         tYPE, primRepToRuntimeRep,
@@ -94,7 +94,7 @@ import {-# SOURCE #-} TysWiredIn
   , doubleElemRepDataConTy
   , mkPromotedListTy )
 
-import Var              ( TyVar, mkTyVar )
+import Var              ( TyVar, TyVarBndr(TvBndr), mkTyVar )
 import Name
 import TyCon
 import SrcLoc
@@ -328,20 +328,21 @@ openBetaTy  = mkTyVarTy openBetaTyVar
 funTyConName :: Name
 funTyConName = mkPrimTyConName (fsLit "(->)") funTyConKey funTyCon
 
+-- | The @(->)@ type constructor.
+--
+-- @
+-- (->) :: forall (rep1 :: RuntimeRep) (rep2 :: RuntimeRep).
+--         TYPE rep1 -> TYPE rep2 -> *
+-- @
 funTyCon :: TyCon
 funTyCon = mkFunTyCon funTyConName tc_bndrs tc_rep_nm
   where
-    tc_bndrs = mkTemplateAnonTyConBinders [liftedTypeKind, liftedTypeKind]
-
-        -- You might think that (->) should have type (?? -> ? -> *), and you'd be right
-        -- But if we do that we get kind errors when saying
-        --      instance Control.Arrow (->)
-        -- because the expected kind is (*->*->*).  The trouble is that the
-        -- expected/actual stuff in the unifier does not go contra-variant, whereas
-        -- the kind sub-typing does.  Sigh.  It really only matters if you use (->) in
-        -- a prefix way, thus:  (->) Int# Int#.  And this is unusual.
-        -- because they are never in scope in the source
-
+    tc_bndrs = [ TvBndr runtimeRep1TyVar (NamedTCB Inferred)
+               , TvBndr runtimeRep2TyVar (NamedTCB Inferred)
+               ]
+               ++ mkTemplateAnonTyConBinders [ tYPE runtimeRep1Ty
+                                             , tYPE runtimeRep2Ty
+                                             ]
     tc_rep_nm = mkPrelTyConRepName funTyConName
 
 {-
diff --git a/compiler/specialise/Rules.hs b/compiler/specialise/Rules.hs
index 168104156f..ae0798ac2b 100644
--- a/compiler/specialise/Rules.hs
+++ b/compiler/specialise/Rules.hs
@@ -810,6 +810,12 @@ match_co renv subst co1 co2
         |  tc1 == tc2
         -> match_cos renv subst cos1 cos2
       _ -> Nothing
+match_co renv subst co1 co2
+  | Just (arg1, res1) <- splitFunCo_maybe co1
+  = case splitFunCo_maybe co2 of
+      Just (arg2, res2)
+        -> match_cos renv subst [arg1, res1] [arg2, res2]
+      _ -> Nothing
 match_co _ _ _co1 _co2
     -- Currently just deals with CoVarCo, TyConAppCo and Refl
 #ifdef DEBUG
diff --git a/compiler/typecheck/TcCanonical.hs b/compiler/typecheck/TcCanonical.hs
index 038b6b9914..c6682081db 100644
--- a/compiler/typecheck/TcCanonical.hs
+++ b/compiler/typecheck/TcCanonical.hs
@@ -33,6 +33,7 @@ import Util
 import Bag
 import MonadUtils
 import Control.Monad
+import Data.Maybe ( isJust )
 import Data.List  ( zip4, foldl' )
 import BasicTypes
 
@@ -540,6 +541,25 @@ track whether or not we've already flattened.
 
 It is conceivable to do a better job at tracking whether or not a type
 is flattened, but this is left as future work. (Mar '15)
+
+
+Note [FunTy and decomposing tycon applications]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+When can_eq_nc' attempts to decompose a tycon application we haven't yet zonked.
+This means that we may very well have a FunTy containing a type of some unknown
+kind. For instance, we may have,
+
+    FunTy (a :: k) Int
+
+Where k is a unification variable. tcRepSplitTyConApp_maybe panics in the event
+that it sees such a type as it cannot determine the RuntimeReps which the (->)
+is applied to. Consequently, it is vital that we instead use
+tcRepSplitTyConApp_maybe', which simply returns Nothing in such a case.
+
+When this happens can_eq_nc' will fail to decompose, zonk, and try again.
+Zonking should fill the variable k, meaning that decomposition will succeed the
+second time around.
 -}
 
 canEqNC :: CtEvidence -> EqRel -> Type -> Type -> TcS (StopOrContinue Ct)
@@ -613,8 +633,9 @@ can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1@(LitTy l1) _ (LitTy l2) _
 -- Try to decompose type constructor applications
 -- Including FunTy (s -> t)
 can_eq_nc' _flat _rdr_env _envs ev eq_rel ty1 _ ty2 _
-  | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
-  , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
+    --- See Note [FunTy and decomposing type constructor applications].
+  | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe' ty1
+  , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe' ty2
   , not (isTypeFamilyTyCon tc1)
   , not (isTypeFamilyTyCon tc2)
   = canTyConApp ev eq_rel tc1 tys1 tc2 tys2
@@ -696,6 +717,26 @@ zonk_eq_types = go
     go (TyVarTy tv1) ty2           = tyvar NotSwapped tv1 ty2
     go ty1 (TyVarTy tv2)           = tyvar IsSwapped  tv2 ty1
 
+    -- We handle FunTys explicitly here despite the fact that they could also be
+    -- treated as an application. Why? Well, for one it's cheaper to just look
+    -- at two types (the argument and result types) than four (the argument,
+    -- result, and their RuntimeReps). Also, we haven't completely zonked yet,
+    -- so we may run into an unzonked type variable while trying to compute the
+    -- RuntimeReps of the argument and result types. This can be observed in
+    -- testcase tc269.
+    go ty1 ty2
+      | Just (arg1, res1) <- split1
+      , Just (arg2, res2) <- split2
+      = do { res_a <- go arg1 arg2
+           ; res_b <- go res1 res2
+           ; return $ combine_rev mkFunTy res_b res_a
+           }
+      | isJust split1 || isJust split2
+      = bale_out ty1 ty2
+      where
+        split1 = tcSplitFunTy_maybe ty1
+        split2 = tcSplitFunTy_maybe ty2
+
     go ty1 ty2
       | Just (tc1, tys1) <- tcRepSplitTyConApp_maybe ty1
       , Just (tc2, tys2) <- tcRepSplitTyConApp_maybe ty2
@@ -1830,7 +1871,7 @@ unifyWanted loc role orig_ty1 orig_ty2
     go (FunTy s1 t1) (FunTy s2 t2)
       = do { co_s <- unifyWanted loc role s1 s2
            ; co_t <- unifyWanted loc role t1 t2
-           ; return (mkTyConAppCo role funTyCon [co_s,co_t]) }
+           ; return (mkFunCo role co_s co_t) }
     go (TyConApp tc1 tys1) (TyConApp tc2 tys2)
       | tc1 == tc2, tys1 `equalLength` tys2
       , isInjectiveTyCon tc1 role -- don't look under newtypes at Rep equality
diff --git a/compiler/typecheck/TcSMonad.hs b/compiler/typecheck/TcSMonad.hs
index 14cb9f20bb..19186c2528 100644
--- a/compiler/typecheck/TcSMonad.hs
+++ b/compiler/typecheck/TcSMonad.hs
@@ -284,7 +284,7 @@ extendWorkListCt :: Ct -> WorkList -> WorkList
 extendWorkListCt ct wl
  = case classifyPredType (ctPred ct) of
      EqPred NomEq ty1 _
-       | Just (tc,_) <- tcSplitTyConApp_maybe ty1
+       | Just tc <- tcTyConAppTyCon_maybe ty1
        , isTypeFamilyTyCon tc
        -> extendWorkListFunEq ct wl
 
diff --git a/compiler/typecheck/TcTyDecls.hs b/compiler/typecheck/TcTyDecls.hs
index 7b69bad264..96154cca8b 100644
--- a/compiler/typecheck/TcTyDecls.hs
+++ b/compiler/typecheck/TcTyDecls.hs
@@ -113,6 +113,7 @@ synonymTyConsOfType ty
      go_co (TyConAppCo _ tc cs)   = go_tc tc `plusNameEnv` go_co_s cs
      go_co (AppCo co co')         = go_co co `plusNameEnv` go_co co'
      go_co (ForAllCo _ co co')    = go_co co `plusNameEnv` go_co co'
+     go_co (FunCo _ co co')       = go_co co `plusNameEnv` go_co co'
      go_co (CoVarCo _)            = emptyNameEnv
      go_co (AxiomInstCo _ _ cs)   = go_co_s cs
      go_co (UnivCo p _ ty ty')    = go_prov p `plusNameEnv` go ty `plusNameEnv` go ty'
diff --git a/compiler/typecheck/TcType.hs b/compiler/typecheck/TcType.hs
index a0ca0b2555..7a87a18939 100644
--- a/compiler/typecheck/TcType.hs
+++ b/compiler/typecheck/TcType.hs
@@ -62,8 +62,9 @@ module TcType (
   tcSplitPhiTy, tcSplitPredFunTy_maybe,
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcFunResultTyN,
   tcSplitFunTysN,
-  tcSplitTyConApp, tcSplitTyConApp_maybe, tcRepSplitTyConApp_maybe,
-  tcTyConAppTyCon, tcTyConAppArgs,
+  tcSplitTyConApp, tcSplitTyConApp_maybe,
+  tcRepSplitTyConApp_maybe, tcRepSplitTyConApp_maybe',
+  tcTyConAppTyCon, tcTyConAppTyCon_maybe, tcTyConAppArgs,
   tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, tcRepSplitAppTy_maybe,
   tcGetTyVar_maybe, tcGetTyVar, nextRole,
   tcSplitSigmaTy, tcSplitNestedSigmaTys, tcDeepSplitSigmaTy_maybe,
@@ -862,6 +863,7 @@ exactTyCoVarsOfType ty
     goCo (AppCo co arg)     = goCo co `unionVarSet` goCo arg
     goCo (ForAllCo tv k_co co)
       = goCo co `delVarSet` tv `unionVarSet` goCo k_co
+    goCo (FunCo _ co1 co2)   = goCo co1 `unionVarSet` goCo co2
     goCo (CoVarCo v)         = unitVarSet v `unionVarSet` go (varType v)
     goCo (AxiomInstCo _ _ args) = goCos args
     goCo (UnivCo p _ t1 t2)  = goProv p `unionVarSet` go t1 `unionVarSet` go t2
@@ -1420,9 +1422,21 @@ tcDeepSplitSigmaTy_maybe ty
 
 -----------------------
 tcTyConAppTyCon :: Type -> TyCon
-tcTyConAppTyCon ty = case tcSplitTyConApp_maybe ty of
-                        Just (tc, _) -> tc
-                        Nothing      -> pprPanic "tcTyConAppTyCon" (pprType ty)
+tcTyConAppTyCon ty
+  = case tcTyConAppTyCon_maybe ty of
+      Just tc -> tc
+      Nothing -> pprPanic "tcTyConAppTyCon" (pprType ty)
+
+-- | Like 'tcRepSplitTyConApp_maybe', but only returns the 'TyCon'.
+tcTyConAppTyCon_maybe :: Type -> Maybe TyCon
+tcTyConAppTyCon_maybe ty
+  | Just ty' <- coreView ty = tcTyConAppTyCon_maybe ty'
+tcTyConAppTyCon_maybe (TyConApp tc _)
+  = Just tc
+tcTyConAppTyCon_maybe (FunTy _ _)
+  = Just funTyCon
+tcTyConAppTyCon_maybe _
+  = Nothing
 
 tcTyConAppArgs :: Type -> [Type]
 tcTyConAppArgs ty = case tcSplitTyConApp_maybe ty of
@@ -1434,14 +1448,48 @@ tcSplitTyConApp ty = case tcSplitTyConApp_maybe ty of
                         Just stuff -> stuff
                         Nothing    -> pprPanic "tcSplitTyConApp" (pprType ty)
 
-tcSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+-- | Split a type constructor application into its type constructor and
+-- applied types. Note that this may fail in the case of a 'FunTy' with an
+-- argument of unknown kind 'FunTy' (e.g. @FunTy (a :: k) Int@. since the kind
+-- of @a@ isn't of the form @TYPE rep@). Consequently, you may need to zonk your
+-- type before using this function.
+--
+-- If you only need the 'TyCon', consider using 'tcTyConAppTyCon_maybe'.
+tcSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 tcSplitTyConApp_maybe ty | Just ty' <- coreView ty = tcSplitTyConApp_maybe ty'
 tcSplitTyConApp_maybe ty                           = tcRepSplitTyConApp_maybe ty
 
-tcRepSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
-tcRepSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-tcRepSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-tcRepSplitTyConApp_maybe _                 = Nothing
+-- | Like 'tcSplitTyConApp_maybe' but doesn't look through type synonyms.
+tcRepSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
+tcRepSplitTyConApp_maybe (TyConApp tc tys)          = Just (tc, tys)
+tcRepSplitTyConApp_maybe (FunTy arg res)
+  | Just arg_rep <- getRuntimeRep_maybe arg
+  , Just res_rep <- getRuntimeRep_maybe res
+  = Just (funTyCon, [arg_rep, res_rep, arg, res])
+
+  | otherwise
+  = pprPanic "tcRepSplitTyConApp_maybe" (ppr arg $$ ppr res)
+tcRepSplitTyConApp_maybe _                          = Nothing
+
+-- | Like 'tcRepSplitTyConApp_maybe', but returns 'Nothing' if,
+--
+-- 1. the type is structurally not a type constructor application, or
+--
+-- 2. the type is a function type (e.g. application of 'funTyCon'), but we
+--    currently don't even enough information to fully determine its RuntimeRep
+--    variables. For instance, @FunTy (a :: k) Int@.
+--
+-- By constrast 'tcRepSplitTyConApp_maybe' panics in the second case.
+--
+-- The behavior here is needed during canonicalization; see Note [FunTy and
+-- decomposing tycon applications] in TcCanonical for details.
+tcRepSplitTyConApp_maybe' :: HasCallStack => Type -> Maybe (TyCon, [Type])
+tcRepSplitTyConApp_maybe' (TyConApp tc tys)          = Just (tc, tys)
+tcRepSplitTyConApp_maybe' (FunTy arg res)
+  | Just arg_rep <- getRuntimeRep_maybe arg
+  , Just res_rep <- getRuntimeRep_maybe res
+  = Just (funTyCon, [arg_rep, res_rep, arg, res])
+tcRepSplitTyConApp_maybe' _                          = Nothing
 
 
 -----------------------
@@ -1627,6 +1675,7 @@ tc_eq_type :: (TcType -> Maybe TcType)  -- ^ @coreView@, if you want unwrapping
            -> Type -> Type -> Maybe Bool
 tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
   where
+    go :: Bool -> RnEnv2 -> Type -> Type -> Maybe Bool
     go vis env t1 t2 | Just t1' <- view_fun t1 = go vis env t1' t2
     go vis env t1 t2 | Just t2' <- view_fun t2 = go vis env t1 t2'
 
@@ -1641,8 +1690,15 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
       = go (isVisibleArgFlag vis1) env (tyVarKind tv1) (tyVarKind tv2)
           <!> go vis (rnBndr2 env tv1 tv2) ty1 ty2
           <!> check vis (vis1 == vis2)
+    -- Make sure we handle all FunTy cases since falling through to the
+    -- AppTy case means that tcRepSplitAppTy_maybe may see an unzonked
+    -- kind variable, which causes things to blow up.
     go vis env (FunTy arg1 res1) (FunTy arg2 res2)
       = go vis env arg1 arg2 <!> go vis env res1 res2
+    go vis env ty (FunTy arg res)
+      = eqFunTy vis env arg res ty
+    go vis env (FunTy arg res) ty
+      = eqFunTy vis env arg res ty
 
       -- See Note [Equality on AppTys] in Type
     go vis env (AppTy s1 t1)        ty2
@@ -1679,6 +1735,28 @@ tc_eq_type view_fun orig_ty1 orig_ty2 = go True orig_env orig_ty1 orig_ty2
 
     orig_env = mkRnEnv2 $ mkInScopeSet $ tyCoVarsOfTypes [orig_ty1, orig_ty2]
 
+    -- @eqFunTy arg res ty@ is True when @ty@ equals @FunTy arg res@. This is
+    -- sometimes hard to know directly because @ty@ might have some casts
+    -- obscuring the FunTy. And 'splitAppTy' is difficult because we can't
+    -- always extract a RuntimeRep (see Note [xyz]) if the kind of the arg or
+    -- res is unzonked/unflattened. Thus this function, which handles this
+    -- corner case.
+    eqFunTy :: Bool -> RnEnv2 -> Type -> Type -> Type -> Maybe Bool
+    eqFunTy vis env arg res (FunTy arg' res')
+      = go vis env arg arg' <!> go vis env res res'
+    eqFunTy vis env arg res ty@(AppTy{})
+      | Just (tc, [_, _, arg', res']) <- get_args ty []
+      , tc == funTyCon
+      = go vis env arg arg' <!> go vis env res res'
+      where
+        get_args :: Type -> [Type] -> Maybe (TyCon, [Type])
+        get_args (AppTy f x)       args = get_args f (x:args)
+        get_args (CastTy t _)      args = get_args t args
+        get_args (TyConApp tc tys) args = Just (tc, tys ++ args)
+        get_args _                 _    = Nothing
+    eqFunTy vis _ _ _ _
+      = Just vis
+
 -- | Like 'pickyEqTypeVis', but returns a Bool for convenience
 pickyEqType :: TcType -> TcType -> Bool
 -- Check when two types _look_ the same, _including_ synonyms.
diff --git a/compiler/typecheck/TcUnify.hs b/compiler/typecheck/TcUnify.hs
index db3233e26f..75732c6f05 100644
--- a/compiler/typecheck/TcUnify.hs
+++ b/compiler/typecheck/TcUnify.hs
@@ -2071,6 +2071,9 @@ occCheckExpand tv ty
                                      env' = extendVarEnv env tv' tv''
                                ; body' <- go_co env' body_co
                                ; return (ForAllCo tv'' kind_co' body') }
+    go_co env (FunCo r co1 co2)         = do { co1' <- go_co env co1
+                                             ; co2' <- go_co env co2
+                                             ; return (mkFunCo r co1' co2') }
     go_co env (CoVarCo c)               = do { k' <- go env (varType c)
                                              ; return (mkCoVarCo (setVarType c k')) }
     go_co env (AxiomInstCo ax ind args) = do { args' <- mapM (go_co env) args
diff --git a/compiler/typecheck/TcValidity.hs b/compiler/typecheck/TcValidity.hs
index fb6bb60fd0..f7cb3197ef 100644
--- a/compiler/typecheck/TcValidity.hs
+++ b/compiler/typecheck/TcValidity.hs
@@ -1900,6 +1900,7 @@ fvCo (Refl _ ty)            = fvType ty
 fvCo (TyConAppCo _ _ args)  = concatMap fvCo args
 fvCo (AppCo co arg)         = fvCo co ++ fvCo arg
 fvCo (ForAllCo tv h co)     = filter (/= tv) (fvCo co) ++ fvCo h
+fvCo (FunCo _ co1 co2)      = fvCo co1 ++ fvCo co2
 fvCo (CoVarCo v)            = [v]
 fvCo (AxiomInstCo _ _ args) = concatMap fvCo args
 fvCo (UnivCo p _ t1 t2)     = fvProv p ++ fvType t1 ++ fvType t2
diff --git a/compiler/types/Coercion.hs b/compiler/types/Coercion.hs
index c7debd4d6f..f5791457ac 100644
--- a/compiler/types/Coercion.hs
+++ b/compiler/types/Coercion.hs
@@ -2,7 +2,7 @@
 (c) The University of Glasgow 2006
 -}
 
-{-# LANGUAGE RankNTypes, CPP, MultiWayIf #-}
+{-# LANGUAGE RankNTypes, CPP, MultiWayIf, FlexibleContexts #-}
 
 -- | Module for (a) type kinds and (b) type coercions,
 -- as used in System FC. See 'CoreSyn.Expr' for
@@ -51,6 +51,7 @@ module Coercion (
         decomposeCo, getCoVar_maybe,
         splitTyConAppCo_maybe,
         splitAppCo_maybe,
+        splitFunCo_maybe,
         splitForAllCo_maybe,
 
         nthRole, tyConRolesX, tyConRolesRepresentational, setNominalRole_maybe,
@@ -107,6 +108,7 @@ module Coercion (
 
 import TyCoRep
 import Type
+import Kind
 import TyCon
 import CoAxiom
 import Var
@@ -114,12 +116,14 @@ import VarEnv
 import Name hiding ( varName )
 import Util
 import BasicTypes
+import FastString
 import Outputable
 import Unique
 import Pair
 import SrcLoc
 import PrelNames
 import TysPrim          ( eqPhantPrimTyCon )
+import {-# SOURCE #-} TysWiredIn ( constraintKind )
 import ListSetOps
 import Maybes
 import UniqFM
@@ -174,13 +178,11 @@ pprParendCo co = ppr_co TyConPrec co
 ppr_co :: TyPrec -> Coercion -> SDoc
 ppr_co _ (Refl r ty) = angleBrackets (ppr ty) <> ppr_role r
 
-ppr_co p co@(TyConAppCo _ tc [_,_])
-  | tc `hasKey` funTyConKey = ppr_fun_co p co
-
 ppr_co _ (TyConAppCo r tc cos) = pprTcAppCo TyConPrec ppr_co tc cos <> ppr_role r
 ppr_co p (AppCo co arg)        = maybeParen p TyConPrec $
                                  pprCo co <+> ppr_co TyConPrec arg
 ppr_co p co@(ForAllCo {})      = ppr_forall_co p co
+ppr_co p co@(FunCo {})         = ppr_fun_co p co
 ppr_co _ (CoVarCo cv)          = parenSymOcc (getOccName cv) (ppr cv)
 ppr_co p (AxiomInstCo con index args)
   = pprPrefixApp p (ppr (getName con) <> brackets (ppr index))
@@ -237,8 +239,7 @@ ppr_fun_co :: TyPrec -> Coercion -> SDoc
 ppr_fun_co p co = pprArrowChain p (split co)
   where
     split :: Coercion -> [SDoc]
-    split (TyConAppCo _ f [arg, res])
-      | f `hasKey` funTyConKey
+    split (FunCo _ arg res)
       = ppr_co FunPrec arg : split res
     split co = [ppr_co TopPrec co]
 
@@ -319,6 +320,8 @@ splitTyConAppCo_maybe (Refl r ty)
        ; let args = zipWith mkReflCo (tyConRolesX r tc) tys
        ; return (tc, args) }
 splitTyConAppCo_maybe (TyConAppCo _ tc cos) = Just (tc, cos)
+splitTyConAppCo_maybe (FunCo _ arg res)     = Just (funTyCon, cos)
+  where cos = [mkRuntimeRepCo arg, mkRuntimeRepCo res, arg, res]
 splitTyConAppCo_maybe _                     = Nothing
 
 -- first result has role equal to input; third result is Nominal
@@ -339,6 +342,10 @@ splitAppCo_maybe (Refl r ty)
   = Just (mkReflCo r ty1, mkNomReflCo ty2)
 splitAppCo_maybe _ = Nothing
 
+splitFunCo_maybe :: Coercion -> Maybe (Coercion, Coercion)
+splitFunCo_maybe (FunCo _ arg res) = Just (arg, res)
+splitFunCo_maybe _ = Nothing
+
 splitForAllCo_maybe :: Coercion -> Maybe (TyVar, Coercion, Coercion)
 splitForAllCo_maybe (ForAllCo tv k_co co) = Just (tv, k_co, co)
 splitForAllCo_maybe _                     = Nothing
@@ -397,6 +404,46 @@ mkHeteroCoercionType Nominal          = mkHeteroPrimEqPred
 mkHeteroCoercionType Representational = mkHeteroReprPrimEqPred
 mkHeteroCoercionType Phantom          = panic "mkHeteroCoercionType"
 
+constraintIsLifted :: CoAxiomRule
+constraintIsLifted =
+    CoAxiomRule { coaxrName = mkFastString "constraintIsLifted"
+                , coaxrAsmpRoles = []
+                , coaxrRole = Nominal
+                , coaxrProves =
+                      const $ Just $ Pair constraintKind liftedTypeKind
+                }
+
+-- | Given a coercion @co1 :: (a :: TYPE r1) ~ (b :: TYPE r2)@,
+-- produce a coercion @rep_co :: r1 ~ r2@.
+mkRuntimeRepCo :: Coercion -> Coercion
+mkRuntimeRepCo co
+    -- This is currently a bit tricky since we can see types of kind Constraint
+    -- in addition to the usual things of kind (TYPE rep). We first map
+    -- Constraint-kinded types to (TYPE 'LiftedRep).
+    -- FIXME: this is terrible
+  | isConstraintKind a && isConstraintKind b
+  = mkNthCo 0 $ constraintToLifted
+  $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+
+  | isConstraintKind a
+  = WARN( True, text "mkRuntimeRepCo" )
+    mkNthCo 0
+  $ mkSymCo $ constraintToLifted $ mkSymCo kind_co
+
+  | isConstraintKind b
+  = WARN( True, text "mkRuntimeRepCo" )
+    mkNthCo 0 $ constraintToLifted kind_co
+
+  | otherwise
+  = mkNthCo 0 kind_co
+  where
+    -- the right side of a coercion from Constraint to TYPE 'LiftedRep
+    constraintToLifted = (`mkTransCo` mkAxiomRuleCo constraintIsLifted [])
+
+    kind_co = mkKindCo co  -- kind_co :: TYPE r1 ~ TYPE r2
+                           -- (up to silliness with Constraint)
+    Pair a b = coercionKind kind_co  -- Pair of (TYPE r1, TYPE r2)
+
 -- | Tests if this coercion is obviously reflexive. Guaranteed to work
 -- very quickly. Sometimes a coercion can be reflexive, but not obviously
 -- so. c.f. 'isReflexiveCo'
@@ -538,8 +585,15 @@ mkNomReflCo = mkReflCo Nominal
 
 -- | Apply a type constructor to a list of coercions. It is the
 -- caller's responsibility to get the roles correct on argument coercions.
-mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
+mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkTyConAppCo r tc cos
+  | tc `hasKey` funTyConKey
+  , [_rep1, _rep2, co1, co2] <- cos
+  = -- (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 co1 co2
+
                -- Expand type synonyms
   | Just (tv_co_prs, rhs_ty, leftover_cos) <- expandSynTyCon_maybe tc cos
   = mkAppCos (liftCoSubst r (mkLiftingContext tv_co_prs) rhs_ty) leftover_cos
@@ -549,9 +603,15 @@ mkTyConAppCo r tc cos
 
   | otherwise = TyConAppCo r tc cos
 
--- | Make a function 'Coercion' between two other 'Coercion's
+-- | 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)@.
 mkFunCo :: Role -> Coercion -> Coercion -> Coercion
-mkFunCo r co1 co2 = mkTyConAppCo r funTyCon [co1, co2]
+mkFunCo r co1 co2
+    -- See Note [Refl invariant]
+  | Just (ty1, _) <- isReflCo_maybe co1
+  , Just (ty2, _) <- isReflCo_maybe co2
+  = Refl r (mkFunTy ty1 ty2)
+  | otherwise = FunCo r co1 co2
 
 -- | Make nested function 'Coercion's
 mkFunCos :: Role -> [Coercion] -> Coercion -> Coercion
@@ -569,7 +629,7 @@ mkAppCo (Refl r ty1) arg
 
   | Just (tc, tys) <- splitTyConApp_maybe ty1
     -- Expand type synonyms; a TyConAppCo can't have a type synonym (Trac #9102)
-  = TyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
+  = mkTyConAppCo r tc (zip_roles (tyConRolesX r tc) tys)
   where
     zip_roles (r1:_)  []            = [downgradeRole r1 Nominal arg]
     zip_roles (r1:rs) (ty1:tys)     = mkReflCo r1 ty1 : zip_roles rs tys
@@ -577,11 +637,11 @@ mkAppCo (Refl r ty1) arg
 
 mkAppCo (TyConAppCo r tc args) arg
   = case r of
-      Nominal          -> TyConAppCo Nominal tc (args ++ [arg])
-      Representational -> TyConAppCo Representational tc (args ++ [arg'])
+      Nominal          -> mkTyConAppCo Nominal tc (args ++ [arg])
+      Representational -> mkTyConAppCo Representational tc (args ++ [arg'])
         where new_role = (tyConRolesRepresentational tc) !! (length args)
               arg'     = downgradeRole new_role Nominal arg
-      Phantom          -> TyConAppCo Phantom tc (args ++ [toPhantomCo arg])
+      Phantom          -> mkTyConAppCo Phantom tc (args ++ [toPhantomCo arg])
 mkAppCo co arg = AppCo co  arg
 -- Note, mkAppCo is careful to maintain invariants regarding
 -- where Refl constructors appear; see the comments in the definition
@@ -839,7 +899,7 @@ mkNthCo 0 (Refl _ ty)
   | Just (tv, _) <- splitForAllTy_maybe ty
   = Refl Nominal (tyVarKind tv)
 mkNthCo n (Refl r ty)
-  = ASSERT( ok_tc_app ty n )
+  = ASSERT2( ok_tc_app ty n, ppr n $$ ppr ty )
     mkReflCo r' (tyConAppArgN n ty)
   where tc = tyConAppTyCon ty
         r' = nthRole r tc n
@@ -857,6 +917,13 @@ mkNthCo 0 (ForAllCo _ kind_co _) = kind_co
   -- If co :: (forall a1:k1. t1) ~ (forall a2:k2. t2)
   -- then (nth 0 co :: k1 ~ k2)
 mkNthCo n (TyConAppCo _ _ arg_cos) = arg_cos `getNth` n
+mkNthCo n co@(FunCo _ arg res)
+  = case n of
+      0 -> mkRuntimeRepCo arg
+      1 -> mkRuntimeRepCo res
+      2 -> arg
+      3 -> res
+      _ -> pprPanic "mkNthCo(FunCo)" (ppr n $$ ppr co)
 mkNthCo n co = NthCo n co
 
 mkLRCo :: LeftOrRight -> Coercion -> Coercion
@@ -894,6 +961,7 @@ infixl 5 `mkCoherenceCo`
 infixl 5 `mkCoherenceRightCo`
 infixl 5 `mkCoherenceLeftCo`
 
+-- | Given @co :: (a :: k) ~ (b :: k')@ produce @co' :: k ~ k'@.
 mkKindCo :: Coercion -> Coercion
 mkKindCo (Refl _ ty) = Refl Nominal (typeKind ty)
 mkKindCo (UnivCo (PhantomProv h) _ _ _)    = h
@@ -913,6 +981,10 @@ mkSubCo :: Coercion -> Coercion
 mkSubCo (Refl Nominal ty) = Refl Representational ty
 mkSubCo (TyConAppCo Nominal tc cos)
   = TyConAppCo Representational tc (applyRoles tc cos)
+mkSubCo (FunCo Nominal arg res)
+  = FunCo Representational
+          (downgradeRole Representational Nominal arg)
+          (downgradeRole Representational Nominal res)
 mkSubCo co = ASSERT2( coercionRole co == Nominal, ppr co <+> ppr (coercionRole co) )
              SubCo co
 
@@ -980,6 +1052,11 @@ setNominalRole_maybe (Refl _ ty) = Just $ Refl Nominal ty
 setNominalRole_maybe (TyConAppCo Representational tc cos)
   = do { cos' <- mapM setNominalRole_maybe cos
        ; return $ TyConAppCo Nominal tc cos' }
+setNominalRole_maybe (FunCo Representational co1 co2)
+  = do { co1' <- setNominalRole_maybe co1
+       ; co2' <- setNominalRole_maybe co2
+       ; return $ FunCo Nominal co1' co2'
+       }
 setNominalRole_maybe (SymCo co)
   = SymCo <$> setNominalRole_maybe co
 setNominalRole_maybe (TransCo co1 co2)
@@ -1088,6 +1165,9 @@ promoteCoercion co = case co of
     ForAllCo _ _ g
       -> promoteCoercion g
 
+    FunCo _ _ _
+      -> mkNomReflCo liftedTypeKind
+
     CoVarCo {}
       -> mkKindCo co
 
@@ -1167,7 +1247,7 @@ instCoercion (Pair lty rty) g w
   , Just w' <- setNominalRole_maybe w
   = Just $ mkInstCo g w'
   | isFunTy lty && isFunTy rty
-  = Just $ mkNthCo 1 g -- extract result type, which is the 2nd argument to (->)
+  = Just $ mkNthCo 3 g -- extract result type, which is the 4th argument to (->)
   | otherwise -- one forall, one funty...
   = Nothing
   where
@@ -1195,6 +1275,8 @@ castCoercionKind g h1 h2
 mkPiCos :: Role -> [Var] -> Coercion -> Coercion
 mkPiCos r vs co = foldr (mkPiCo r) co vs
 
+-- | Make a forall 'Coercion', where both types related by the coercion
+-- are quantified over the same type variable.
 mkPiCo  :: Role -> Var -> Coercion -> Coercion
 mkPiCo r v co | isTyVar v = mkHomoForAllCos [v] co
               | otherwise = mkFunCo r (mkReflCo r (varType v)) co
@@ -1640,6 +1722,7 @@ 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 (tyVarKind tv) `seq` seqCo k
                                                          `seq` seqCo co
+seqCo (FunCo r co1 co2)         = r `seq` seqCo co1 `seq` seqCo co2
 seqCo (CoVarCo cv)              = cv `seq` ()
 seqCo (AxiomInstCo con ind cos) = con `seq` ind `seq` seqCos cos
 seqCo (UnivCo p r t1 t2)
@@ -1714,6 +1797,7 @@ coercionKind co = go co
             -- This is doing repeated substitutions and probably doesn't
             -- need to, see #11735
         mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2'
+    go (FunCo _ co1 co2)    = mkFunTy <$> go co1 <*> go co2
     go (CoVarCo cv)         = toPair $ coVarTypes cv
     go (AxiomInstCo ax ind cos)
       | CoAxBranch { cab_tvs = tvs, cab_cvs = cvs
@@ -1794,6 +1878,8 @@ coercionKindRole = go
             -- This is doing repeated substitutions and probably doesn't
             -- need to, see #11735
         (mkInvForAllTy <$> Pair tv1 tv2 <*> Pair ty1 ty2', r)
+    go (FunCo r co1 co2)
+      = (mkFunTy <$> coercionKind co1 <*> coercionKind co2, r)
     go (CoVarCo cv) = (toPair $ coVarTypes cv, coVarRole cv)
     go co@(AxiomInstCo ax _ _) = (coercionKind co, coAxiomRole ax)
     go (UnivCo _ r ty1 ty2)  = (Pair ty1 ty2, r)
@@ -1811,7 +1897,7 @@ coercionKindRole = go
       = let (tc1,  args1) = splitTyConApp ty1
             (_tc2, args2) = splitTyConApp ty2
         in
-        ASSERT( tc1 == _tc2 )
+        ASSERT2( tc1 == _tc2, ppr d $$ ppr tc1 $$ ppr _tc2 )
         ((`getNth` d) <$> Pair args1 args2, nthRole r tc1 d)
 
       where
diff --git a/compiler/types/Coercion.hs-boot b/compiler/types/Coercion.hs-boot
index 8ba92952b4..eefefd09e8 100644
--- a/compiler/types/Coercion.hs-boot
+++ b/compiler/types/Coercion.hs-boot
@@ -1,3 +1,5 @@
+{-# LANGUAGE FlexibleContexts #-}
+
 module Coercion where
 
 import {-# SOURCE #-} TyCoRep
@@ -8,11 +10,13 @@ import CoAxiom
 import Var
 import Outputable
 import Pair
+import Util
 
 mkReflCo :: Role -> Type -> Coercion
-mkTyConAppCo :: Role -> TyCon -> [Coercion] -> Coercion
+mkTyConAppCo :: HasDebugCallStack => Role -> TyCon -> [Coercion] -> Coercion
 mkAppCo :: Coercion -> Coercion -> Coercion
 mkForAllCo :: TyVar -> Coercion -> Coercion -> Coercion
+mkFunCo :: Role -> Coercion -> Coercion -> Coercion
 mkCoVarCo :: CoVar -> Coercion
 mkAxiomInstCo :: CoAxiom Branched -> BranchIndex -> [Coercion] -> Coercion
 mkPhantomCo :: Coercion -> Type -> Type -> Coercion
diff --git a/compiler/types/FamInstEnv.hs b/compiler/types/FamInstEnv.hs
index e605f7b4fd..89f4214766 100644
--- a/compiler/types/FamInstEnv.hs
+++ b/compiler/types/FamInstEnv.hs
@@ -1693,6 +1693,7 @@ allTyVarsInTy = go
     go_co (AppCo co arg)        = go_co co `unionVarSet` go_co arg
     go_co (ForAllCo tv h co)
       = unionVarSets [unitVarSet tv, go_co co, go_co h]
+    go_co (FunCo _ c1 c2)       = go_co c1 `unionVarSet` go_co c2
     go_co (CoVarCo cv)          = unitVarSet cv
     go_co (AxiomInstCo _ _ cos) = go_cos cos
     go_co (UnivCo p _ t1 t2)    = go_prov p `unionVarSet` go t1 `unionVarSet` go t2
diff --git a/compiler/types/OptCoercion.hs b/compiler/types/OptCoercion.hs
index 5e1f4547d9..5e4927fb70 100644
--- a/compiler/types/OptCoercion.hs
+++ b/compiler/types/OptCoercion.hs
@@ -207,6 +207,15 @@ 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 co1 co2)
+  = ASSERT( r == _r )
+    if rep
+    then mkFunCo Representational co1' co2'
+    else mkFunCo r co1' co2'
+  where
+    co1' = opt_co4_wrap env sym rep r co1
+    co2' = opt_co4_wrap env sym rep r co2
+
 opt_co4 env sym rep r (CoVarCo cv)
   | Just co <- lookupCoVar (lcTCvSubst env) cv
   = opt_co4_wrap (zapLiftingContext env) sym rep r co
diff --git a/compiler/types/TyCoRep.hs b/compiler/types/TyCoRep.hs
index e4c1c979cb..1e90fa7aee 100644
--- a/compiler/types/TyCoRep.hs
+++ b/compiler/types/TyCoRep.hs
@@ -441,7 +441,8 @@ Pi-types:
 
  * A non-dependent function type,
    written with ->, e.g. ty1 -> ty2
-   represented as FunTy ty1 ty2
+   represented as FunTy ty1 ty2. These are
+   lifted to Coercions with the corresponding FunCo.
 
  * A dependent compile-time-only polytype,
    written with forall, e.g.  forall (a:*). ty
@@ -790,6 +791,9 @@ data Coercion
   | ForAllCo TyVar KindCoercion Coercion
          -- ForAllCo :: _ -> N -> e -> e
 
+  | FunCo Role Coercion Coercion         -- lift FunTy
+         -- FunCo :: "e" -> e -> e -> e
+
   -- These are special
   | CoVarCo CoVar      -- :: _ -> (N or R)
                        -- result role depends on the tycon of the variable's type
@@ -1440,6 +1444,8 @@ tyCoFVsOfCo (AppCo co arg) fv_cand in_scope acc
   = (tyCoFVsOfCo co `unionFV` tyCoFVsOfCo arg) fv_cand in_scope acc
 tyCoFVsOfCo (ForAllCo tv kind_co co) fv_cand in_scope acc
   = (delFV tv (tyCoFVsOfCo co) `unionFV` tyCoFVsOfCo kind_co) fv_cand in_scope acc
+tyCoFVsOfCo (FunCo _ co1 co2)    fv_cand in_scope acc
+  = (tyCoFVsOfCo co1 `unionFV` tyCoFVsOfCo co2) fv_cand in_scope acc
 tyCoFVsOfCo (CoVarCo v) fv_cand in_scope acc
   = (unitFV v `unionFV` tyCoFVsOfType (varType v)) fv_cand in_scope acc
 tyCoFVsOfCo (AxiomInstCo _ _ cos) fv_cand in_scope acc = tyCoFVsOfCos cos fv_cand in_scope acc
@@ -1500,6 +1506,7 @@ coVarsOfCo (TyConAppCo _ _ args) = coVarsOfCos args
 coVarsOfCo (AppCo co arg)      = coVarsOfCo co `unionVarSet` coVarsOfCo arg
 coVarsOfCo (ForAllCo tv kind_co co)
   = coVarsOfCo co `delVarSet` tv `unionVarSet` coVarsOfCo kind_co
+coVarsOfCo (FunCo _ co1 co2)   = coVarsOfCo co1 `unionVarSet` coVarsOfCo co2
 coVarsOfCo (CoVarCo v)         = unitVarSet v `unionVarSet` coVarsOfType (varType v)
 coVarsOfCo (AxiomInstCo _ _ args) = coVarsOfCos args
 coVarsOfCo (UnivCo p _ t1 t2)  = coVarsOfProv p `unionVarSet` coVarsOfTypes [t1, t2]
@@ -1566,6 +1573,7 @@ noFreeVarsOfCo (Refl _ ty)            = noFreeVarsOfType ty
 noFreeVarsOfCo (TyConAppCo _ _ args)  = all noFreeVarsOfCo args
 noFreeVarsOfCo (AppCo c1 c2)          = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
 noFreeVarsOfCo co@(ForAllCo {})       = isEmptyVarSet (tyCoVarsOfCo co)
+noFreeVarsOfCo (FunCo _ c1 c2)        = noFreeVarsOfCo c1 && noFreeVarsOfCo c2
 noFreeVarsOfCo (CoVarCo _)            = False
 noFreeVarsOfCo (AxiomInstCo _ _ args) = all noFreeVarsOfCo args
 noFreeVarsOfCo (UnivCo p _ t1 t2)     = noFreeVarsOfProv p &&
@@ -2234,6 +2242,7 @@ subst_co subst co
     go (ForAllCo tv kind_co co)
       = case substForAllCoBndrUnchecked subst tv kind_co of { (subst', tv', kind_co') ->
           ((mkForAllCo $! tv') $! kind_co') $! subst_co subst' co }
+    go (FunCo r co1 co2)     = (mkFunCo r $! go co1) $! go co2
     go (CoVarCo cv)          = substCoVar subst cv
     go (AxiomInstCo con ind cos) = mkAxiomInstCo con ind $! map go cos
     go (UnivCo p r t1 t2)    = (((mkUnivCo $! go_prov p) $! r) $!
@@ -2771,6 +2780,7 @@ tidyCo env@(_, subst) co
                                where (envp, tvp) = tidyTyCoVarBndr env tv
             -- the case above duplicates a bit of work in tidying h and the kind
             -- of tv. But the alternative is to use coercionKind, which seems worse.
+    go (FunCo r co1 co2)     = (FunCo r $! go co1) $! go co2
     go (CoVarCo cv)          = case lookupVarEnv subst cv of
                                  Nothing  -> CoVarCo cv
                                  Just cv' -> CoVarCo cv'
@@ -2833,6 +2843,7 @@ coercionSize (Refl _ ty)         = typeSize ty
 coercionSize (TyConAppCo _ _ args) = 1 + sum (map coercionSize args)
 coercionSize (AppCo co arg)      = coercionSize co + coercionSize arg
 coercionSize (ForAllCo _ h co)   = 1 + coercionSize co + coercionSize h
+coercionSize (FunCo _ co1 co2)   = 1 + coercionSize co1 + coercionSize co2
 coercionSize (CoVarCo _)         = 1
 coercionSize (AxiomInstCo _ _ args) = 1 + sum (map coercionSize args)
 coercionSize (UnivCo p _ t1 t2)  = 1 + provSize p + typeSize t1 + typeSize t2
diff --git a/compiler/types/TyCon.hs b/compiler/types/TyCon.hs
index 3aa2805616..1b80d20ad4 100644
--- a/compiler/types/TyCon.hs
+++ b/compiler/types/TyCon.hs
@@ -1391,7 +1391,7 @@ So we compromise, and move their Kind calculation to the call site.
 -}
 
 -- | Given the name of the function type constructor and it's kind, create the
--- corresponding 'TyCon'. It is reccomended to use 'TyCoRep.funTyCon' if you want
+-- corresponding 'TyCon'. It is recomended to use 'TyCoRep.funTyCon' if you want
 -- this functionality
 mkFunTyCon :: Name -> [TyConBinder] -> Name -> TyCon
 mkFunTyCon name binders rep_nm
@@ -1401,7 +1401,7 @@ mkFunTyCon name binders rep_nm
         tyConBinders = binders,
         tyConResKind = liftedTypeKind,
         tyConKind    = mkTyConKind binders liftedTypeKind,
-        tyConArity   = 2,
+        tyConArity   = length binders,
         tcRepName    = rep_nm
     }
 
diff --git a/compiler/types/Type.hs b/compiler/types/Type.hs
index 2cce7fe415..a50b76b2a3 100644
--- a/compiler/types/Type.hs
+++ b/compiler/types/Type.hs
@@ -47,6 +47,8 @@ module Type (
         mkNumLitTy, isNumLitTy,
         mkStrLitTy, isStrLitTy,
 
+        getRuntimeRep_maybe, getRuntimeRepFromKind_maybe,
+
         mkCastTy, mkCoercionTy, splitCastTy_maybe,
 
         userTypeError_maybe, pprUserTypeErrorTy,
@@ -385,6 +387,8 @@ expandTypeSynonyms ty
     go_co subst (ForAllCo tv kind_co co)
       = let (subst', tv', kind_co') = go_cobndr subst tv kind_co in
         mkForAllCo tv' kind_co' (go_co subst' co)
+    go_co subst (FunCo r co1 co2)
+      = mkFunCo r (go_co subst co1) (go_co subst co2)
     go_co subst (CoVarCo cv)
       = substCoVar subst cv
     go_co subst (AxiomInstCo ax ind args)
@@ -520,6 +524,7 @@ mapCoercion mapper@(TyCoMapper { tcm_smart = smart, tcm_covar = covar
            ; co' <- mapCoercion mapper env' co
            ; return $ mkforallco tv' kind_co' co' }
         -- See Note [Efficiency for mapCoercion ForAllCo case]
+    go (FunCo r c1 c2) = mkFunCo r <$> go c1 <*> go c2
     go (CoVarCo cv) = covar env cv
     go (AxiomInstCo ax i args)
       = mkaxiominstco ax i <$> mapM go args
@@ -660,8 +665,15 @@ splitAppTy_maybe ty = repSplitAppTy_maybe ty
 repSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'splitAppTy_maybe', but assumes that
 -- any Core view stuff is already done
-repSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
-repSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
+repSplitAppTy_maybe (FunTy ty1 ty2)
+  | Just rep1 <- getRuntimeRep_maybe ty1
+  , Just rep2 <- getRuntimeRep_maybe ty2
+  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
+
+  | otherwise
+  = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
+repSplitAppTy_maybe (AppTy ty1 ty2)
+  = Just (ty1, ty2)
 repSplitAppTy_maybe (TyConApp tc tys)
   | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
   , Just (tys', ty') <- snocView tys
@@ -675,9 +687,16 @@ tcRepSplitAppTy_maybe :: Type -> Maybe (Type,Type)
 -- ^ Does the AppTy split as in 'tcSplitAppTy_maybe', but assumes that
 -- any coreView stuff is already done. Refuses to look through (c => t)
 tcRepSplitAppTy_maybe (FunTy ty1 ty2)
-  | isConstraintKind (typeKind ty1)     = Nothing  -- See Note [Decomposing fat arrow c=>t]
-  | otherwise                           = Just (TyConApp funTyCon [ty1], ty2)
-tcRepSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
+  | isConstraintKind (typeKind ty1)
+  = Nothing  -- See Note [Decomposing fat arrow c=>t]
+
+  | Just rep1 <- getRuntimeRep_maybe ty1
+  , Just rep2 <- getRuntimeRep_maybe ty2
+  = Just (TyConApp funTyCon [rep1, rep2, ty1], ty2)
+
+  | otherwise
+  = pprPanic "repSplitAppTy_maybe" (ppr ty1 $$ ppr ty2)
+tcRepSplitAppTy_maybe (AppTy ty1 ty2)    = Just (ty1, ty2)
 tcRepSplitAppTy_maybe (TyConApp tc tys)
   | mightBeUnsaturatedTyCon tc || tys `lengthExceeds` tyConArity tc
   , Just (tys', ty') <- snocView tys
@@ -707,9 +726,15 @@ splitAppTys ty = split ty ty []
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
-    split _   (FunTy ty1 ty2) args = ASSERT( null args )
-                                     (TyConApp funTyCon [], [ty1,ty2])
-    split orig_ty _           args = (orig_ty, args)
+    split _   (FunTy ty1 ty2) args
+      | Just rep1 <- getRuntimeRep_maybe ty1
+      , Just rep2 <- getRuntimeRep_maybe ty2
+      = ASSERT( null args )
+        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
+
+      | otherwise
+      = pprPanic "splitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
+    split orig_ty _                     args  = (orig_ty, args)
 
 -- | Like 'splitAppTys', but doesn't look through type synonyms
 repSplitAppTys :: Type -> (Type, [Type])
@@ -722,8 +747,14 @@ repSplitAppTys ty = split ty []
             (tc_args1, tc_args2) = splitAt n tc_args
         in
         (TyConApp tc tc_args1, tc_args2 ++ args)
-    split (FunTy ty1 ty2) args = ASSERT( null args )
-                                 (TyConApp funTyCon [], [ty1, ty2])
+    split (FunTy ty1 ty2) args
+      | Just rep1 <- getRuntimeRep_maybe ty1
+      , Just rep2 <- getRuntimeRep_maybe ty2
+      = ASSERT( null args )
+        (TyConApp funTyCon [], [rep1, rep2, ty1, ty2])
+
+      | otherwise
+      = pprPanic "repSplitAppTys" (ppr ty1 $$ ppr ty2 $$ ppr args)
     split ty args = (ty, args)
 
 {-
@@ -795,6 +826,34 @@ pprUserTypeErrorTy ty =
 ---------------------------------------------------------------------
                                 FunTy
                                 ~~~~~
+
+Note [Representation of function types]
+~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
+
+Functions (e.g. Int -> Char) are can be thought of as being applications
+of funTyCon (known in Haskell surface syntax as (->)),
+
+    (->) :: forall (r1 :: RuntimeRep) (r2 :: RuntimeRep)
+                   (a :: TYPE r1) (b :: TYPE r2).
+            a -> b -> Type
+
+However, for efficiency's sake we represent saturated applications of (->)
+with FunTy. For instance, the type,
+
+    (->) r1 r2 a b
+
+is equivalent to,
+
+    FunTy (Anon a) b
+
+Note how the RuntimeReps are implied in the FunTy representation. For this
+reason we must be careful when recontructing the TyConApp representation (see,
+for instance, splitTyConApp_maybe).
+
+In the compiler we maintain the invariant that all saturated applications of
+(->) are represented with FunTy.
+
+See #11714.
 -}
 
 isFunTy :: Type -> Bool
@@ -937,7 +996,8 @@ applyTysX tvs body_ty arg_tys
 -- its arguments.  Applies its arguments to the constructor from left to right.
 mkTyConApp :: TyCon -> [Type] -> Type
 mkTyConApp tycon tys
-  | isFunTyCon tycon, [ty1,ty2] <- tys
+  | isFunTyCon tycon
+  , [_rep1,_rep2,ty1,ty2] <- tys
   = FunTy ty1 ty2
 
   | otherwise
@@ -969,7 +1029,10 @@ tyConAppTyCon ty = tyConAppTyCon_maybe ty `orElse` pprPanic "tyConAppTyCon" (ppr
 tyConAppArgs_maybe :: Type -> Maybe [Type]
 tyConAppArgs_maybe ty | Just ty' <- coreView ty = tyConAppArgs_maybe ty'
 tyConAppArgs_maybe (TyConApp _ tys) = Just tys
-tyConAppArgs_maybe (FunTy arg res)  = Just [arg,res]
+tyConAppArgs_maybe (FunTy arg res)
+  | Just rep1 <- getRuntimeRep_maybe arg
+  , Just rep2 <- getRuntimeRep_maybe res
+  = Just [rep1, rep2, arg, res]
 tyConAppArgs_maybe _                = Nothing
 
 tyConAppArgs :: Type -> [Type]
@@ -992,16 +1055,22 @@ splitTyConApp ty = case splitTyConApp_maybe ty of
 
 -- | Attempts to tease a type apart into a type constructor and the application
 -- of a number of arguments to that constructor
-splitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+splitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 splitTyConApp_maybe ty | Just ty' <- coreView ty = splitTyConApp_maybe ty'
 splitTyConApp_maybe ty                           = repSplitTyConApp_maybe ty
 
 -- | Like 'splitTyConApp_maybe', but doesn't look through synonyms. This
 -- assumes the synonyms have already been dealt with.
-repSplitTyConApp_maybe :: Type -> Maybe (TyCon, [Type])
+repSplitTyConApp_maybe :: HasCallStack => Type -> Maybe (TyCon, [Type])
 repSplitTyConApp_maybe (TyConApp tc tys) = Just (tc, tys)
-repSplitTyConApp_maybe (FunTy arg res)   = Just (funTyCon, [arg,res])
-repSplitTyConApp_maybe _                 = Nothing
+repSplitTyConApp_maybe (FunTy arg res)
+  | Just rep1 <- getRuntimeRep_maybe arg
+  , Just rep2 <- getRuntimeRep_maybe res
+  = Just (funTyCon, [rep1, rep2, arg, res])
+  | otherwise
+  = pprPanic "repSplitTyConApp_maybe"
+             (ppr arg $$ ppr res $$ ppr (typeKind res))
+repSplitTyConApp_maybe _ = Nothing
 
 -- | Attempts to tease a list type apart and gives the type of the elements if
 -- successful (looks through type synonyms)
@@ -1101,6 +1170,7 @@ mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
                  ASSERT2( CastTy ty co `eqType` result
                         , ppr ty <+> dcolon <+> ppr (typeKind ty) $$
                           ppr co <+> dcolon <+> ppr (coercionKind co) $$
+                          ppr (CastTy ty co) <+> dcolon <+> ppr (typeKind (CastTy ty co)) $$
                           ppr result <+> dcolon <+> ppr (typeKind result) )
                  result
   where
@@ -1119,8 +1189,10 @@ mkCastTy ty co = -- NB: don't check if the coercion "from" type matches here;
                  saturated_tc (decomp_args `chkAppend` args) co
 
     split_apps args (FunTy arg res) co
+      | rep_arg <- getRuntimeRep "mkCastTy.split_apps" arg
+      , rep_res <- getRuntimeRep "mkCastTy.split_apps" res
       = affix_co (tyConTyBinders funTyCon) (mkTyConTy funTyCon)
-                 (arg : res : args) co
+                 (rep_arg : rep_res : arg : res : args) co
     split_apps args ty co
       = affix_co (fst $ splitPiTys $ typeKind ty)
                  ty args co
@@ -1888,27 +1960,47 @@ isUnliftedType ty
   = not (isLiftedType_maybe ty `orElse`
          pprPanic "isUnliftedType" (ppr ty <+> dcolon <+> ppr (typeKind ty)))
 
--- | Extract the RuntimeRep classifier of a type. Panics if this is not possible.
+-- | Extract the RuntimeRep classifier of a type. For instance,
+-- @getRuntimeRep_maybe Int = LiftedRep@. Returns 'Nothing' if this is not
+-- possible.
+getRuntimeRep_maybe :: HasDebugCallStack
+                    => Type -> Maybe Type
+getRuntimeRep_maybe = getRuntimeRepFromKind_maybe . typeKind
+
+-- | Extract the RuntimeRep classifier of a type. For instance,
+-- @getRuntimeRep_maybe Int = LiftedRep@. Panics if this is not possible.
 getRuntimeRep :: HasDebugCallStack
               => String   -- ^ Printed in case of an error
               -> Type -> Type
-getRuntimeRep err ty = getRuntimeRepFromKind err (typeKind ty)
-
--- | Extract the RuntimeRep classifier of a type from its kind.
--- For example, getRuntimeRepFromKind * = LiftedRep;
--- Panics if this is not possible.
+getRuntimeRep err ty =
+    case getRuntimeRep_maybe ty of
+      Just r  -> r
+      Nothing -> pprPanic "getRuntimeRep"
+                          (text err $$ ppr ty <+> dcolon <+> ppr (typeKind ty))
+
+-- | Extract the RuntimeRep classifier of a type from its kind. For example,
+-- @getRuntimeRepFromKind * = LiftedRep@; Panics if this is not possible.
 getRuntimeRepFromKind :: HasDebugCallStack
-                      => String  -- ^ Printed in case of an error
-                      -> Type -> Type
-getRuntimeRepFromKind err = go
+                      => String -> Type -> Type
+getRuntimeRepFromKind err k =
+    case getRuntimeRepFromKind_maybe k of
+      Just r  -> r
+      Nothing -> pprPanic "getRuntimeRepFromKind"
+                          (text err $$ ppr k <+> dcolon <+> ppr (typeKind k))
+
+-- | Extract the RuntimeRep classifier of a type from its kind. For example,
+-- @getRuntimeRepFromKind * = LiftedRep@; Returns 'Nothing' if this is not
+-- possible.
+getRuntimeRepFromKind_maybe :: HasDebugCallStack
+                            => Type -> Maybe Type
+getRuntimeRepFromKind_maybe = go
   where
     go k | Just k' <- coreViewOneStarKind k = go k'
     go k
-      | (_tc, [arg]) <- splitTyConApp k
-      = ASSERT2( _tc `hasKey` tYPETyConKey, text err $$ ppr k )
-        arg
-    go k = pprPanic "getRuntimeRep" (text err $$
-                                     ppr k <+> dcolon <+> ppr (typeKind k))
+      | Just (_tc, [arg]) <- splitTyConApp_maybe k
+      = ASSERT2( _tc `hasKey` tYPETyConKey, ppr k )
+        Just arg
+    go _ = Nothing
 
 isUnboxedTupleType :: Type -> Bool
 isUnboxedTupleType ty
@@ -2170,6 +2262,7 @@ nonDetCmpTypeX env orig_t1 orig_t2 =
     go _   (LitTy l1)          (LitTy l2)          = liftOrdering (compare l1 l2)
     go env (CastTy t1 _)       t2                  = hasCast $ go env t1 t2
     go env t1                  (CastTy t2 _)       = hasCast $ go env t1 t2
+
     go _   (CoercionTy {})     (CoercionTy {})     = TEQ
 
         -- Deal with the rest: TyVarTy < CoercionTy < AppTy < LitTy < TyConApp < ForAllTy
@@ -2291,6 +2384,7 @@ tyConsOfType ty
      go_co (TyConAppCo _ tc args)  = go_tc tc `plusNameEnv` go_cos args
      go_co (AppCo co arg)          = go_co co `plusNameEnv` go_co arg
      go_co (ForAllCo _ kind_co co) = go_co kind_co `plusNameEnv` go_co co
+     go_co (FunCo _ co1 co2)       = go_co co1 `plusNameEnv` go_co co2
      go_co (CoVarCo {})            = emptyNameEnv
      go_co (AxiomInstCo ax _ args) = go_ax ax `plusNameEnv` go_cos args
      go_co (UnivCo p _ t1 t2)      = go_prov p `plusNameEnv` go t1 `plusNameEnv` go t2
diff --git a/compiler/types/Unify.hs b/compiler/types/Unify.hs
index 0ee895a4ba..41b8c6138d 100644
--- a/compiler/types/Unify.hs
+++ b/compiler/types/Unify.hs
@@ -1162,8 +1162,8 @@ data MatchEnv = ME { me_tmpls :: TyVarSet
                    , me_env   :: RnEnv2 }
 
 -- | 'liftCoMatch' is sort of inverse to 'liftCoSubst'.  In particular, if
---   @liftCoMatch vars ty co == Just s@, then @tyCoSubst s ty == co@,
---   where @==@ there means that the result of tyCoSubst has the same
+--   @liftCoMatch vars ty co == Just s@, then @listCoSubst s ty == co@,
+--   where @==@ there means that the result of 'liftCoSubst' has the same
 --   type as the original co; but may be different under the hood.
 --   That is, it matches a type against a coercion of the same
 --   "shape", and returns a lifting substitution which could have been
@@ -1269,8 +1269,15 @@ ty_co_match menv subst ty1 (AppCo co2 arg2) _lkco _rkco
 
 ty_co_match menv subst (TyConApp tc1 tys) (TyConAppCo _ tc2 cos) _lkco _rkco
   = ty_co_match_tc menv subst tc1 tys tc2 cos
-ty_co_match menv subst (FunTy ty1 ty2) (TyConAppCo _ tc cos) _lkco _rkco
-  = ty_co_match_tc menv subst funTyCon [ty1, ty2] tc cos
+ty_co_match menv subst (FunTy ty1 ty2) co _lkco _rkco
+    -- Despite the fact that (->) is polymorphic in four type variables (two
+    -- runtime rep and two types), we shouldn't need to explicitly unify the
+    -- runtime reps here; unifying the types themselves should be sufficient.
+    -- See Note [Representation of function types].
+  | Just (tc, [_,_,co1,co2]) <- splitTyConAppCo_maybe co
+  , tc == funTyCon
+  = let Pair lkcos rkcos = traverse (fmap mkNomReflCo . coercionKind) [co1,co2]
+    in ty_co_match_args menv subst [ty1, ty2] [co1, co2] lkcos rkcos
 
 ty_co_match menv subst (ForAllTy (TvBndr tv1 _) ty1)
                        (ForAllCo tv2 kind_co2 co2)
@@ -1334,7 +1341,10 @@ pushRefl :: Coercion -> Maybe Coercion
 pushRefl (Refl Nominal (AppTy ty1 ty2))
   = Just (AppCo (Refl Nominal ty1) (mkNomReflCo ty2))
 pushRefl (Refl r (FunTy ty1 ty2))
-  = Just (TyConAppCo r funTyCon [mkReflCo r ty1, mkReflCo r ty2])
+  | Just rep1 <- getRuntimeRep_maybe ty1
+  , Just rep2 <- getRuntimeRep_maybe ty2
+  = Just (TyConAppCo r funTyCon [ mkReflCo r rep1, mkReflCo r rep2
+                                , mkReflCo r ty1,  mkReflCo r ty2 ])
 pushRefl (Refl r (TyConApp tc tys))
   = Just (TyConAppCo r tc (zipWith mkReflCo (tyConRolesX r tc) tys))
 pushRefl (Refl r (ForAllTy (TvBndr tv _) ty))
diff --git a/libraries/base/tests/all.T b/libraries/base/tests/all.T
index 7125b636f8..8e5125fc3b 100644
--- a/libraries/base/tests/all.T
+++ b/libraries/base/tests/all.T
@@ -119,7 +119,7 @@ test('T2528', normal, compile_and_run, [''])
 test('T4006', normal, compile_and_run, [''])
 
 test('T5943', normal, compile_and_run, [''])
-test('T5962', normal, compile_and_run, [''])
+test('T5962', expect_broken(10343), compile_and_run, [''])
 test('T7034', normal, compile_and_run, [''])
 
 test('qsem001', normal, compile_and_run, [''])
diff --git a/testsuite/tests/ghci/scripts/T8535.stdout b/testsuite/tests/ghci/scripts/T8535.stdout
index 7245bf2d3d..2aea35f3de 100644
--- a/testsuite/tests/ghci/scripts/T8535.stdout
+++ b/testsuite/tests/ghci/scripts/T8535.stdout
@@ -1,4 +1,4 @@
-data (->) a b 	-- Defined in ‘GHC.Prim’
+data (->) (a :: TYPE q) (b :: TYPE r) 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Applicative ((->) a) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/scripts/ghci020.stdout b/testsuite/tests/ghci/scripts/ghci020.stdout
index 7245bf2d3d..2aea35f3de 100644
--- a/testsuite/tests/ghci/scripts/ghci020.stdout
+++ b/testsuite/tests/ghci/scripts/ghci020.stdout
@@ -1,4 +1,4 @@
-data (->) a b 	-- Defined in ‘GHC.Prim’
+data (->) (a :: TYPE q) (b :: TYPE r) 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Applicative ((->) a) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/ghci/should_run/T10145.stdout b/testsuite/tests/ghci/should_run/T10145.stdout
index 7245bf2d3d..2aea35f3de 100644
--- a/testsuite/tests/ghci/should_run/T10145.stdout
+++ b/testsuite/tests/ghci/should_run/T10145.stdout
@@ -1,4 +1,4 @@
-data (->) a b 	-- Defined in ‘GHC.Prim’
+data (->) (a :: TYPE q) (b :: TYPE r) 	-- Defined in ‘GHC.Prim’
 infixr 0 `(->)`
 instance Monoid b => Monoid (a -> b) -- Defined in ‘GHC.Base’
 instance Applicative ((->) a) -- Defined in ‘GHC.Base’
diff --git a/testsuite/tests/partial-sigs/should_compile/T10403.stderr b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
index 0588c1b5bc..3027d17d1b 100644
--- a/testsuite/tests/partial-sigs/should_compile/T10403.stderr
+++ b/testsuite/tests/partial-sigs/should_compile/T10403.stderr
@@ -41,7 +41,8 @@ T10403.hs:22:15: warning: [-Wdeferred-type-errors (in -Wdefault)]
         instance Functor IO -- Defined in ‘GHC.Base’
         instance Functor (B t) -- Defined at T10403.hs:10:10
         instance Functor I -- Defined at T10403.hs:6:10
-        ...plus four others
+        ...plus three others
+        ...plus one instance involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the second argument of ‘(.)’, namely ‘fmap (const ())’
       In the expression: H . fmap (const ())
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 0592bd6800..5f898fbbee 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -737,13 +737,14 @@ test('T9675',
 test('T9872a',
      [ only_ways(['normal']),
        compiler_stats_num_field('bytes allocated',
-          [(wordsize(64), 3134866040    , 5),
+          [(wordsize(64), 3304620816, 5),
           # 2014-12-10    5521332656    Initally created
           # 2014-12-16    5848657456    Flattener parameterized over roles
           # 2014-12-18    2680733672    Reduce type families even more eagerly
           # 2015-12-11    3581500440    TypeInType (see #11196)
           # 2016-04-07    3352882080    CSE improvements
           # 2016-10-19    3134866040    Refactor traceRn interface (#12617)
+          # 2017-02-01    3304620816
            (wordsize(32), 1740903516, 5)
           # was           1325592896
           # 2016-04-06    1740903516    x86/Linux
diff --git a/testsuite/tests/perf/haddock/all.T b/testsuite/tests/perf/haddock/all.T
index 5ed6758cfc..4c641d5828 100644
--- a/testsuite/tests/perf/haddock/all.T
+++ b/testsuite/tests/perf/haddock/all.T
@@ -5,7 +5,7 @@
 test('haddock.base',
      [unless(in_tree_compiler(), skip), req_haddock
      ,stats_num_field('bytes allocated',
-          [(wordsize(64), 32695562088, 5)
+          [(wordsize(64), 38425793776, 5)
             # 2012-08-14:  5920822352 (amd64/Linux)
             # 2012-09-20:  5829972376 (amd64/Linux)
             # 2012-10-08:  5902601224 (amd64/Linux)
@@ -33,6 +33,7 @@ test('haddock.base',
             # 2017-01-11: 31115778088 (x86_64/Linux) - Join points (#12988)
             # 2017-02-11: 34819979936 (x86_64/Linux) - OccurAnal / One-Shot  (#13227)
             # 2017-02-16: 32695562088 Better Lint for join points
+            # 2017-02-17: 38425793776 (x86_64/Linux) - Generalize kind of (->)
 
           ,(platform('i386-unknown-mingw32'), 4434804940, 5)
             # 2013-02-10:                     3358693084 (x86/Windows)
@@ -55,7 +56,7 @@ test('haddock.base',
 test('haddock.Cabal',
      [unless(in_tree_compiler(), skip), req_haddock
      ,stats_num_field('bytes allocated',
-          [(wordsize(64), 23867276992, 5)
+          [(wordsize(64), 27784875792, 5)
             # 2012-08-14:  3255435248 (amd64/Linux)
             # 2012-08-29:  3324606664 (amd64/Linux, new codegen)
             # 2012-10-08:  3373401360 (amd64/Linux)
@@ -98,6 +99,7 @@ test('haddock.Cabal',
             # 2017-01-14: 23272708864 (amd64/Linux) - Join points (#12988)
             # 2017-02-11: 25533642168 (amd64/Linux) - OccurAnal / One-Shot  (#13227)
             # 2017-02-16: 23867276992  Better Lint for join points
+            # 2017-02-17: 27784875792 (amd64/Linux) - Generalize kind of (->)
 
           ,(platform('i386-unknown-mingw32'), 3293415576, 5)
             # 2012-10-30:                     1733638168 (x86/Windows)
diff --git a/testsuite/tests/typecheck/should_compile/all.T b/testsuite/tests/typecheck/should_compile/all.T
index c44ab9153c..8a5610d848 100644
--- a/testsuite/tests/typecheck/should_compile/all.T
+++ b/testsuite/tests/typecheck/should_compile/all.T
@@ -167,7 +167,7 @@ test('tc163', normal, compile, [''])
 test('tc164', normal, compile, [''])
 test('tc165', expect_broken_for(10181, ['optasm', 'optllvm']), compile, [''])
 test('tc166', normal, compile, [''])
-test('tc167', normal, compile_fail, [''])
+test('tc167', normal, compile, [''])
 test('tc168', normal, compile_fail, [''])
 test('tc169', normal, compile, [''])
 
diff --git a/testsuite/tests/typecheck/should_compile/tc167.stderr b/testsuite/tests/typecheck/should_compile/tc167.stderr
deleted file mode 100644
index 634b50dd5b..0000000000
--- a/testsuite/tests/typecheck/should_compile/tc167.stderr
+++ /dev/null
@@ -1,6 +0,0 @@
-
-tc167.hs:8:15:
-    Expecting a lifted type, but ‘Int#’ is unlifted
-    In the first argument of ‘(->)’, namely ‘Int#’
-    In the type ‘(->) Int#’
-    In the type declaration for ‘T’
diff --git a/testsuite/tests/typecheck/should_fail/tcfail181.stderr b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
index 30e27b8bb7..3ab08676b5 100644
--- a/testsuite/tests/typecheck/should_fail/tcfail181.stderr
+++ b/testsuite/tests/typecheck/should_fail/tcfail181.stderr
@@ -9,8 +9,9 @@ tcfail181.hs:17:9: error:
       These potential instances exist:
         instance Monad IO -- Defined in ‘GHC.Base’
         instance Monad Maybe -- Defined in ‘GHC.Base’
-        instance Monad ((->) r) -- Defined in ‘GHC.Base’
-        ...plus two others
+        instance Monoid a => Monad ((,) a) -- Defined in ‘GHC.Base’
+        ...plus one other
+        ...plus one instance involving out-of-scope types
         (use -fprint-potential-instances to see them all)
     • In the expression: foo
       In the expression: foo {bar = return True}