Add some perf tests for coercions

  This patch adds some performance tests for programs that create
  large coercions. This is useful because the existing test coverage
  is not very representative of real-world situations. In particular,
  this adds a test involving an extensible records library, a common
  pain-point for users.

9 files changed, 1189 insertions, 0 deletions

diff --git a/testsuite/tests/perf/compiler/LargeRecord.hs b/testsuite/tests/perf/compiler/LargeRecord.hs
new file mode 100644
index 0000000000..6b238b54de
--- /dev/null
+++ b/testsuite/tests/perf/compiler/LargeRecord.hs
@@ -0,0 +1,84 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE OverloadedLabels #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+
+{-# OPTIONS_GHC -freduction-depth=0 #-}
+
+module DCo_Record where
+
+import SuperRecord
+
+type BigFieldList =
+  '[ "f1" := Int
+   , "f2" := Int
+   , "f3" := Int
+   , "f4" := Int
+   , "f5" := Int
+   , "f6" := Int
+   , "f7" := Int
+   , "f8" := Int
+   , "f9" := Int
+   , "f10" := Int
+   , "f11" := Int
+   , "f12" := Int
+   , "f13" := Int
+   , "f14" := Int
+   , "f15" := Int
+   , "f16" := Int
+   , "f17" := Int
+   , "f18" := Int
+   , "f19" := Int
+   , "f20" := Int
+   , "f21" := Int
+   , "f22" := Int
+   , "f23" := Int
+   , "f24" := Int
+   , "f25" := Int
+   , "f26" := Int
+   , "f27" := Int
+   , "f28" := Int
+   , "f29" := Int
+   , "f30" := Int
+   ]
+
+bigRec :: Record BigFieldList
+bigRec =
+    #f1   := 1
+  & #f2   := 2
+  & #f3   := 3
+  & #f4   := 4
+  & #f5   := 5
+  & #f6   := 6
+  & #f7   := 7
+  & #f8   := 8
+  & #f9   := 9
+  & #f10  := 10
+  & #f11  := 11
+  & #f12  := 12
+  & #f13  := 13
+  & #f14  := 14
+  & #f15  := 15
+  & #f16  := 16
+  & #f17  := 17
+  & #f18  := 18
+  & #f19  := 19
+  & #f20  := 20
+  & #f21  := 21
+  & #f22  := 22
+  & #f23  := 23
+  & #f24  := 24
+  & #f25  := 25
+  & #f26  := 26
+  & #f27  := 27
+  & #f28  := 28
+  & #f29  := 29
+  & #f30  := 30
+  & rnil
+
+main :: IO ()
+main = print "ok"
diff --git a/testsuite/tests/perf/compiler/SuperRecord.hs b/testsuite/tests/perf/compiler/SuperRecord.hs
new file mode 100644
index 0000000000..3730a49e31
--- /dev/null
+++ b/testsuite/tests/perf/compiler/SuperRecord.hs
@@ -0,0 +1,603 @@
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE ExistentialQuantification #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UnboxedTuples #-}
+{-# LANGUAGE MagicHash #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+module SuperRecord where
+
+import Data.Proxy
+import Data.Typeable
+import Data.Kind
+import GHC.Base ( IO(..) )
+import GHC.Exts
+import GHC.Generics
+import GHC.OverloadedLabels
+import GHC.TypeLits
+import System.IO.Unsafe ( unsafePerformIO )
+
+-- | Field named @l@ labels value of type @t@ adapted from the awesome /labels/ package.
+-- Example: @(#name := \"Chris\") :: (\"name\" := String)@
+data label := value = KnownSymbol label => FldProxy label := !value
+infix 6 :=
+
+instance (Eq value) => Eq (label := value) where
+  (_ := x) == (_ := y) = x == y
+  {-# INLINE (==) #-}
+
+instance (Ord value) => Ord (label := value) where
+  compare (_ := x) (_ := y) = x `compare` y
+  {-# INLINE compare #-}
+
+instance (Show t) =>
+         Show (l := t) where
+  showsPrec p (l := t) =
+      showParen (p > 10) (showString ("#" ++ symbolVal l ++ " := " ++ show t))
+
+-- | A proxy witness for a label. Very similar to 'Proxy', but needed to implement
+-- a non-orphan 'IsLabel' instance
+data FldProxy (t :: Symbol)
+    = FldProxy
+    deriving (Show, Read, Eq, Ord, Typeable)
+
+instance l ~ l' => IsLabel (l :: Symbol) (FldProxy l') where
+    fromLabel = FldProxy
+
+
+-- | The core record type. Prefer this type when manually writing type
+-- signatures
+type Record lts = Rec (Sort lts)
+
+-- | Internal record type. When manually writing an explicit type signature for
+-- a record, use 'Record' instead. For abstract type signatures 'Rec' will work
+-- well.
+data Rec (lts :: [Type])
+   = Rec { _unRec :: SmallArray# Any } -- Note that the values are physically in reverse order
+
+instance (RecApply lts lts Show) => Show (Rec lts) where
+    show = show . showRec
+
+instance RecEq lts lts => Eq (Rec lts) where
+    (==) (a :: Rec lts) (b :: Rec lts) = recEq a b (Proxy :: Proxy lts)
+    {-# INLINE (==) #-}
+
+-- | An empty record
+rnil :: Rec '[]
+rnil = unsafeRnil 0
+{-# INLINE rnil #-}
+
+-- | An empty record with an initial size for the record
+unsafeRnil :: Int -> Rec '[]
+unsafeRnil (I# n#) =
+    unsafePerformIO $! IO $ \s# ->
+    case newSmallArray# n# (error "No Value") s# of
+      (# s'#, arr# #) ->
+          case unsafeFreezeSmallArray# arr# s'# of
+            (# s''#, a# #) -> (# s''# , Rec a# #)
+{-# INLINE unsafeRnil #-}
+
+-- | Prepend a record entry to a record 'Rec'
+rcons ::
+    forall l t lts s.
+    ( RecSize lts ~ s
+    , KnownNat s
+    , KnownNat (RecVecIdxPos l (Sort (l := t ': lts)))
+    , KeyDoesNotExist l lts
+    , RecCopy lts lts (Sort (l := t ': lts))
+    )
+    => l := t -> Rec lts -> Rec (Sort (l := t ': lts))
+rcons (_ := val) lts =
+    unsafePerformIO $! IO $ \s# ->
+    case newSmallArray# newSize# (error "No value") s# of
+      (# s'#, arr# #) ->
+          case recCopyInto (Proxy :: Proxy lts) lts (Proxy :: Proxy (Sort (l := t ': lts))) arr# s'# of
+            s''# ->
+                case writeSmallArray# arr# setAt# (unsafeCoerce# val) s''# of
+                  s'''# ->
+                      case unsafeFreezeSmallArray# arr# s'''# of
+                        (# s''''#, a# #) -> (# s''''#, Rec a# #)
+    where
+        !(I# setAt#) =
+            fromIntegral (natVal' (proxy# :: Proxy# (RecVecIdxPos l (Sort (l := t ': lts)))))
+        newSize# = size# +# 1#
+        !(I# size#) = fromIntegral $ natVal' (proxy# :: Proxy# s)
+{-# INLINE rcons #-}
+
+class RecCopy (pts :: [Type]) (lts :: [Type]) (rts :: [Type]) where
+    recCopyInto ::
+        Proxy pts -> Rec lts -> Proxy rts
+        -> SmallMutableArray# RealWorld Any
+        -> State# RealWorld
+        -> State# RealWorld
+
+instance RecCopy '[] lts rts where
+    recCopyInto _ _ _ _ s# = s#
+
+instance
+    ( Has l rts t
+    , Has l lts t
+    , RecCopy (RemoveAccessTo l (l := t ': pts)) lts rts
+    ) => RecCopy (l := t ': pts) lts rts where
+    recCopyInto _ lts prxy tgt# s# =
+        let lbl :: FldProxy l
+            lbl = FldProxy
+            val = get lbl lts
+            pNext :: Proxy (RemoveAccessTo l (l := t ': pts))
+            pNext = Proxy
+            !(I# setAt#) =
+                fromIntegral (natVal' (proxy# :: Proxy# (RecVecIdxPos l rts)))
+        in case writeSmallArray# tgt# setAt# (unsafeCoerce# val) s# of
+             s'# -> recCopyInto pNext lts prxy tgt# s'#
+
+-- | Prepend a record entry to a record 'Rec'. Assumes that the record was created with
+-- 'unsafeRnil' and still has enough free slots, mutates the original 'Rec' which should
+-- not be reused after
+unsafeRCons ::
+    forall l t lts s.
+    (RecSize lts ~ s, KnownNat s, KeyDoesNotExist l lts)
+    => l := t -> Rec lts -> Rec (l := t ': lts)
+unsafeRCons (_ := val) (Rec vec#) =
+    unsafePerformIO $! IO $ \s# ->
+    case unsafeThawSmallArray# vec# s# of
+      (# s'#, arr# #) ->
+          case writeSmallArray# arr# size# (unsafeCoerce# val) s'# of
+            s''# ->
+                case unsafeFreezeSmallArray# arr# s''# of
+                  (# s'''#, a# #) -> (# s'''#, Rec a# #)
+    where
+        !(I# size#) = fromIntegral $ natVal' (proxy# :: Proxy# s)
+{-# INLINE unsafeRCons #-}
+
+-- | Alias for 'rcons'
+(&) ::
+    forall l t lts s.
+    ( RecSize lts ~ s
+    , KnownNat s
+    , KnownNat (RecVecIdxPos l (Sort (l := t ': lts)))
+    , KeyDoesNotExist l lts
+    , RecCopy lts lts (Sort (l := t ': lts))
+    )
+    => l := t -> Rec lts -> Rec (Sort (l := t ': lts))
+(&) = rcons
+{-# INLINE (&) #-}
+
+infixr 5 &
+
+type family Sort (lts :: [Type]) where
+    Sort '[] = '[]
+    Sort (x := t ': xs) = SortInsert (x := t) (Sort xs)
+
+type family SortInsert (x :: Type) (xs :: [Type]) where
+    SortInsert x '[] = x ': '[]
+    SortInsert (x := t) ((y := u) ': ys) = SortInsert' (CmpSymbol x y) (x := t) (y := u) ys
+
+type family SortInsert' (b :: Ordering) (x :: Type) (y :: Type) (ys :: [Type]) where
+    SortInsert' 'LT  x y ys = x ': (y ': ys)
+    SortInsert' _    x y ys = y ': SortInsert x ys
+
+type family KeyDoesNotExist (l :: Symbol) (lts :: [Type]) :: Constraint where
+    KeyDoesNotExist l '[] = 'True ~ 'True
+    KeyDoesNotExist l (l := t ': lts) =
+        TypeError
+        ( 'Text "Duplicate key " ':<>: 'Text l
+        )
+    KeyDoesNotExist q (l := t ': lts) = KeyDoesNotExist q lts
+
+type RecAppend lhs rhs = RecAppendH lhs rhs rhs '[]
+
+type family ListConcat (xs :: [Type]) (ys :: [Type]) :: [Type] where
+    ListConcat '[] ys = ys
+    ListConcat xs '[] = xs
+    ListConcat (x ': xs) ys = x ': (ListConcat xs ys)
+
+type family ListReverse (xs :: [Type]) :: [Type] where
+    ListReverse (x ': xs) = ListConcat (ListReverse xs) '[x]
+    ListReverse '[] = '[]
+
+type family RecAppendH (lhs ::[Type]) (rhs :: [Type]) (rhsall :: [Type]) (accum :: [Type]) :: [Type] where
+    RecAppendH (l := t ': lhs) (m := u ': rhs) rhsall acc = RecAppendH (l := t ': lhs) rhs rhsall acc
+    RecAppendH (l := t ': lhs) '[] rhsall acc = RecAppendH lhs rhsall rhsall (l := t ': acc)
+    RecAppendH '[] rhs rhsall acc = ListConcat (ListReverse acc) rhsall
+
+type family RecSize (lts :: [Type]) :: Nat where
+    RecSize '[] = 0
+    RecSize (l := t ': lts) = 1 + RecSize lts
+
+type RecVecIdxPos l lts = RecSize lts - RecTyIdxH 0 l lts - 1
+
+type family RecTyIdxH (i :: Nat) (l :: Symbol) (lts :: [Type]) :: Nat where
+    RecTyIdxH idx l (l := t ': lts) = idx
+    RecTyIdxH idx m (l := t ': lts) = RecTyIdxH (1 + idx) m lts
+    RecTyIdxH idx m '[] =
+        TypeError
+        ( 'Text "Could not find label "
+          ':<>: 'Text m
+        )
+
+type RecTy :: forall k. Symbol -> [Type] -> k
+type family RecTy l lts where
+    RecTy l (l := t ': lts) = t
+    RecTy q (l := t ': lts) = RecTy q lts
+
+-- | Require a record to contain at least the listed labels
+type family HasOf (req :: [Type]) (lts :: [Type]) :: Constraint where
+    HasOf (l := t ': req) lts = (Has l lts t, HasOf req lts)
+    HasOf '[] lts = 'True ~ 'True
+
+-- | Require a record to contain a label
+type Has l lts v =
+   ( RecTy l lts ~ v
+   , KnownNat (RecSize lts)
+   , KnownNat (RecVecIdxPos l lts)
+   )
+
+-- | Get an existing record field
+get ::
+    forall l v lts.
+    ( Has l lts v )
+    => FldProxy l -> Rec lts -> v
+get _ (Rec vec#) =
+    let !(I# readAt#) =
+            fromIntegral (natVal' (proxy# :: Proxy# (RecVecIdxPos l lts)))
+        anyVal :: Any
+        anyVal =
+           case indexSmallArray# vec# readAt# of
+             (# a# #) -> a#
+    in unsafeCoerce# anyVal
+{-# INLINE get #-}
+
+-- | Alias for 'get'
+(&.) :: forall l v lts. (Has l lts v) => Rec lts -> FldProxy l -> v
+(&.) = flip get
+infixl 3 &.
+
+-- | Update an existing record field
+set ::
+    forall l v lts.
+    (Has l lts v)
+    => FldProxy l -> v -> Rec lts -> Rec lts
+set _ !val (Rec vec#) =
+    let !(I# size#) = fromIntegral $ natVal' (proxy# :: Proxy# (RecSize lts))
+        !(I# setAt#) = fromIntegral (natVal' (proxy# :: Proxy# (RecVecIdxPos l lts)))
+        dynVal :: Any
+        !dynVal = unsafeCoerce# val
+        r2 =
+            unsafePerformIO $! IO $ \s# ->
+            case newSmallArray# size# (error "No value") s# of
+              (# s'#, arr# #) ->
+                  case copySmallArray# vec# 0# arr# 0# size# s'# of
+                    s''# ->
+                        case writeSmallArray# arr# setAt# dynVal s''# of
+                          s'''# ->
+                              case unsafeFreezeSmallArray# arr# s'''# of
+                                (# s''''#, a# #) -> (# s''''#, Rec a# #)
+    in r2
+{-# INLINE set #-}
+
+-- | Update an existing record field
+modify ::
+    forall l v lts.
+    (Has l lts v)
+    => FldProxy l -> (v -> v) -> Rec lts -> Rec lts
+modify lbl fun r = set lbl (fun $ get lbl r) r
+{-# INLINE modify #-}
+
+-- | Constructor for field accessor paths
+data lbl :& more = FldProxy lbl :& more
+infixr 8 :&
+
+-- | Constructor for field accessor paths
+(&:) :: FldProxy q -> more -> q :& more
+(&:) = (:&)
+{-# INLINE (&:) #-}
+
+infixr 8 &:
+
+-- | Specialized version of (&:) to help writing the last piece of the path w/o
+-- confusing the type checker
+(&:-) :: FldProxy q -> FldProxy r -> q :& FldProxy r
+(&:-) = (:&)
+{-# INLINE (&:-) #-}
+
+infixr 8 &:-
+
+-- | Helper function to allow to clearing specify unknown 'IsLabel' cases
+fld :: FldProxy l -> FldProxy l
+fld = id
+
+type RecDeepTy :: forall r. r -> [Type] -> Type
+type family RecDeepTy ps lts where
+    RecDeepTy (l :& more) (l := Rec t ': lts) = RecDeepTy more t
+    RecDeepTy (l :& more) (l := t ': lts) = t
+    RecDeepTy (l :& more) (q := t ': lts) = RecDeepTy (l :& more) lts
+    RecDeepTy (FldProxy l) '[l := t] = t
+    RecDeepTy l '[l := t] = t
+
+class RecApplyPath p x where
+    -- | Perform a deep update, setting the key along the path to the
+    -- desired value
+    setPath' :: p -> (RecDeepTy p x -> RecDeepTy p x) -> Rec x -> Rec x
+
+    -- | Perform a deep read
+    getPath' :: p -> Rec x -> RecDeepTy p x
+
+instance (Has l lts t, t ~ RecDeepTy (FldProxy l) lts) => RecApplyPath (FldProxy l) lts where
+    setPath' = modify
+    {-# INLINE setPath' #-}
+
+    getPath' = get
+    {-# INLINE getPath' #-}
+
+instance
+    ( RecDeepTy (l :& more) lts ~ RecDeepTy more rts
+    , RecTy l lts ~ Rec rts
+    , Has l lts v
+    , v ~ Rec rts
+    , RecApplyPath more rts
+    ) => RecApplyPath (l :& more) lts where
+    setPath' (x :& more) v r =
+        let innerVal :: Rec rts
+            innerVal = get x r
+        in set x (setPath' more v innerVal) r
+    {-# INLINE setPath' #-}
+
+    getPath' (x :& more) r = getPath' more (get x r)
+    {-# INLINE getPath' #-}
+
+-- | Perform a deep update, setting the key along the path to the
+-- desired value
+setPath :: RecApplyPath k x => k -> RecDeepTy k x -> Rec x -> Rec x
+setPath s v = setPath' s (const v)
+{-# INLINE setPath #-}
+
+-- | Perform a deep update, transforming the value at the final key
+modifyPath :: RecApplyPath k x => k -> (RecDeepTy k x -> RecDeepTy k x) -> Rec x -> Rec x
+modifyPath = setPath'
+{-# INLINE modifyPath #-}
+
+-- | Perform a deep read. This is somewhat similar to using (&.), but is useful
+-- when you want to share a 'RecPath' between 'getPath', 'modifyPath' and/or 'setPath'
+getPath :: RecApplyPath k x => k -> Rec x -> RecDeepTy k x
+getPath = getPath'
+{-# INLINE getPath #-}
+
+-- | Combine two records
+combine ::
+    forall lhs rhs.
+    ( KnownNat (RecSize lhs)
+    , KnownNat (RecSize rhs)
+    , KnownNat (RecSize lhs + RecSize rhs)
+    , RecCopy lhs lhs (Sort (RecAppend lhs rhs))
+    , RecCopy rhs rhs (Sort (RecAppend lhs rhs))
+    )
+    => Rec lhs
+    -> Rec rhs
+    -> Rec (Sort (RecAppend lhs rhs))
+combine lts rts =
+    let !(I# size#) =
+            fromIntegral $ natVal' (proxy# :: Proxy# (RecSize lhs + RecSize rhs))
+    in unsafePerformIO $! IO $ \s# ->
+            case newSmallArray# size# (error "No value") s# of
+              (# s'#, arr# #) ->
+                  case recCopyInto (Proxy :: Proxy lhs) lts (Proxy :: Proxy (Sort (RecAppend lhs rhs))) arr# s'# of
+                    s''# ->
+                        case recCopyInto (Proxy :: Proxy rhs) rts (Proxy :: Proxy (Sort (RecAppend lhs rhs))) arr# s''# of
+                          s'''# ->
+                              case unsafeFreezeSmallArray# arr# s'''# of
+                                (# s''''#, a# #) -> (# s''''#, Rec a# #)
+{-# INLINE combine #-}
+
+-- | Alias for 'combine'
+(++:) ::
+    forall lhs rhs.
+    ( KnownNat (RecSize lhs)
+    , KnownNat (RecSize rhs)
+    , KnownNat (RecSize lhs + RecSize rhs)
+    , RecCopy lhs lhs (Sort (RecAppend lhs rhs))
+    , RecCopy rhs rhs (Sort (RecAppend lhs rhs))
+    )
+    => Rec lhs
+    -> Rec rhs
+    -> Rec (Sort (RecAppend lhs rhs))
+(++:) = combine
+{-# INLINE (++:) #-}
+
+data RecFields (flds :: [Symbol]) where
+    RFNil :: RecFields '[]
+    RFCons :: KnownSymbol f => FldProxy f -> RecFields xs -> RecFields (f ': xs)
+
+recKeys :: forall t (lts :: [Type]). RecKeys lts => t lts -> [String]
+recKeys = recKeys' . recFields
+
+recKeys' :: RecFields lts -> [String]
+recKeys' x =
+    case x of
+      RFNil -> []
+      RFCons q qs -> symbolVal q : recKeys' qs
+
+-- | Get keys of a record on value and type level
+class RecKeys (lts :: [Type]) where
+    type RecKeysT lts :: [Symbol]
+    recFields :: t lts -> RecFields (RecKeysT lts)
+
+instance RecKeys '[] where
+    type RecKeysT '[] = '[]
+    recFields _ = RFNil
+
+instance (KnownSymbol l, RecKeys lts) => RecKeys (l := t ': lts) where
+    type RecKeysT (l := t ': lts) = (l ': RecKeysT lts)
+    recFields (_ :: f (l := t ': lts)) =
+        let lbl :: FldProxy l
+            lbl = FldProxy
+            more :: Proxy lts
+            more = Proxy
+        in (lbl `RFCons` recFields more)
+
+-- | Apply a function to each key element pair for a record
+reflectRec ::
+    forall c r lts. (RecApply lts lts c)
+    => Proxy c
+    -> (forall a. c a => String -> a -> r)
+    -> Rec lts
+    -> [r]
+reflectRec _ f r =
+    reverse $
+    recApply (\(Dict :: Dict (c a)) s v xs -> (f s v : xs)) r (Proxy :: Proxy lts) []
+{-# INLINE reflectRec #-}
+
+-- | Fold over all elements of a record
+reflectRecFold ::
+    forall c r lts. (RecApply lts lts c)
+    => Proxy c
+    -> (forall a. c a => String -> a -> r -> r)
+    -> Rec lts
+    -> r
+    -> r
+reflectRecFold _ f r =
+    recApply (\(Dict :: Dict (c a)) s v x -> f s v x) r (Proxy :: Proxy lts)
+{-# INLINE reflectRecFold #-}
+
+-- | Convert all elements of a record to a 'String'
+showRec :: forall lts. (RecApply lts lts Show) => Rec lts -> [(String, String)]
+showRec = reflectRec @Show Proxy (\k v -> (k, show v))
+
+-- | Machinery needed to implement 'reflectRec'
+class RecApply (rts :: [Type]) (lts :: [Type]) c where
+    recApply :: (forall a. Dict (c a) -> String -> a -> b -> b) -> Rec rts -> Proxy lts -> b -> b
+
+instance RecApply rts '[] c where
+    recApply _ _ _ b = b
+
+instance
+    ( KnownSymbol l
+    , RecApply rts (RemoveAccessTo l lts) c
+    , Has l rts v
+    , c v
+    ) => RecApply rts (l := t ': lts) c where
+    recApply f r (_ :: Proxy (l := t ': lts)) b =
+        let lbl :: FldProxy l
+            lbl = FldProxy
+            val = get lbl r
+            res = f Dict (symbolVal lbl) val b
+            pNext :: Proxy (RemoveAccessTo l (l := t ': lts))
+            pNext = Proxy
+        in recApply f r pNext res
+
+-- | Machinery to implement equality
+class RecEq (rts :: [Type]) (lts :: [Type]) where
+    recEq :: Rec rts -> Rec rts -> Proxy lts -> Bool
+
+instance RecEq rts '[] where
+    recEq _ _ _ = True
+
+instance
+    ( RecEq rts (RemoveAccessTo l lts)
+    , Has l rts v
+    , Eq v
+    ) => RecEq rts (l := t ': lts) where
+    recEq r1 r2 (_ :: Proxy (l := t ': lts)) =
+       let lbl :: FldProxy l
+           lbl = FldProxy
+           val = get lbl r1
+           val2 = get lbl r2
+           res = val == val2
+           pNext :: Proxy (RemoveAccessTo l (l := t ': lts))
+           pNext = Proxy
+       in res && recEq r1 r2 pNext
+
+type family RemoveAccessTo (l :: Symbol) (lts :: [Type]) :: [Type] where
+    RemoveAccessTo l (l := t ': lts) = RemoveAccessTo l lts
+    RemoveAccessTo q (l := t ': lts) = (l := t ': RemoveAccessTo l lts)
+    RemoveAccessTo q '[] = '[]
+
+-- | Conversion helper to bring a Haskell type to a record. Note that the
+-- native Haskell type must be an instance of 'Generic'
+class FromNative a lts | a -> lts where
+    fromNative' :: a x -> Rec lts
+
+instance FromNative cs lts => FromNative (D1 m cs) lts where
+    fromNative' (M1 xs) = fromNative' xs
+
+instance FromNative cs lts => FromNative (C1 m cs) lts where
+    fromNative' (M1 xs) = fromNative' xs
+
+instance
+    KnownSymbol name
+    => FromNative (S1 ('MetaSel ('Just name) p s l) (Rec0 t)) '[name := t]
+    where
+    fromNative' (M1 (K1 t)) = (FldProxy :: FldProxy name) := t & rnil
+
+instance
+    ( FromNative l lhs
+    , FromNative r rhs
+    , lts ~ Sort (RecAppend lhs rhs)
+    , RecCopy lhs lhs lts
+    , RecCopy rhs rhs lts
+    , KnownNat (RecSize lhs)
+    , KnownNat (RecSize rhs)
+    , KnownNat (RecSize lhs + RecSize rhs)
+    )
+    => FromNative (l :*: r) lts where
+    fromNative' (l :*: r) = fromNative' l ++: fromNative' r
+
+-- | Convert a native Haskell type to a record
+fromNative :: (Generic a, FromNative (Rep a) lts) => a -> Rec lts
+fromNative = fromNative' . from
+{-# INLINE fromNative #-}
+
+-- | Conversion helper to bring a record back into a Haskell type. Note that the
+-- native Haskell type must be an instance of 'Generic'
+class ToNative a lts where
+    toNative' :: Rec lts -> a x
+
+instance ToNative cs lts => ToNative (D1 m cs) lts where
+    toNative' xs = M1 $ toNative' xs
+
+instance ToNative cs lts => ToNative (C1 m cs) lts where
+    toNative' xs = M1 $ toNative' xs
+
+instance
+    (Has name lts t)
+    => ToNative (S1 ('MetaSel ('Just name) p s l) (Rec0 t)) lts
+    where
+    toNative' r =
+        M1 $ K1 (get (FldProxy :: FldProxy name) r)
+
+instance
+    ( ToNative l lts
+    , ToNative r lts
+    )
+    => ToNative (l :*: r) lts where
+    toNative' r = toNative' r :*: toNative' r
+
+-- | Convert a record to a native Haskell type
+toNative :: (Generic a, ToNative (Rep a) lts) => Rec lts -> a
+toNative = to . toNative'
+{-# INLINE toNative #-}
+
+type Lens s t a b = forall f. Functor f => (a -> f b) -> (s -> f t)
+
+-- | Convert a field label to a lens
+lens ::
+    Has l lts v => FldProxy l -> Lens (Rec lts) (Rec lts) v v
+lens lbl f r =
+    fmap (\v -> set lbl v r) (f (get lbl r))
+{-# INLINE lens #-}
+
+data Dict c where
+  Dict :: c => Dict c
diff --git a/testsuite/tests/perf/compiler/T13386.hs b/testsuite/tests/perf/compiler/T13386.hs
new file mode 100644
index 0000000000..68d681c19f
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T13386.hs
@@ -0,0 +1,20 @@
+{-# LANGUAGE DataKinds, TypeApplications, TypeFamilies, TypeOperators, UndecidableInstances #-}
+{-# OPTIONS_GHC -O0 -freduction-depth=500 #-}
+
+module T13386 where
+
+import GHC.TypeLits
+
+type DivisibleBy x y = Help x y 0 (CmpNat x 0)
+
+type family Help x y z b where
+  Help x y z EQ = True
+  Help x y z LT = False
+  Help x y z GT = Help x y (z+y) (CmpNat x z)
+
+foo :: DivisibleBy y 3 ~ True => proxy y -> ()
+foo _ = ()
+
+type N = 1002
+
+k = foo @N undefined
diff --git a/testsuite/tests/perf/compiler/T15703.hs b/testsuite/tests/perf/compiler/T15703.hs
new file mode 100644
index 0000000000..98f4388b0f
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T15703.hs
@@ -0,0 +1,154 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneKindSignatures #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15703 where
+
+import Data.Kind
+import Data.Type.Equality
+import GHC.Generics
+import T15703_aux
+
+-----
+-- The important bits
+-----
+
+-- DefaultSignatures-based instances
+instance PMonoid a => PApplicative ((,) a)
+instance SMonoid a => SApplicative ((,) a)
+instance VMonoid a => VApplicative ((,) a)
+
+instance SApplicative f => SApplicative (M1 i c f) where
+  sPure x = singFun3 @(.@#@$) (%.) @@ singFun1 @M1Sym0 SM1 @@ (singFun1 @PureSym0 sPure) @@ x
+  -- If I change the implementation of sPure above to be this:
+  --
+  --   sPure x = SM1 (sPure x)
+  --
+  -- Then T15703.hs compiles quickly again (< 1 second) with -O1.
+
+  SM1 f %<*> SM1 x = SM1 (f %<*> x)
+
+-------------------------------------------------------------------------------
+
+type GenericPure :: a -> f a
+type family GenericPure (x :: a) :: f a where
+  GenericPure x = To1 (Pure x)
+
+type GenericPureC (f :: Type -> Type) (x :: a) =
+  (Pure x :: f a) ~ (GenericPure x :: f a)
+
+type GenericAp :: f (a ~> b) -> f a -> f b
+type family (g :: f (a ~> b)) `GenericAp` (x :: f a) :: f b where
+  g `GenericAp` x = To1 (From1 g <*> From1 x)
+
+type GenericApC (g :: f (a ~> b)) (x :: f a) =
+  (g <*> x) ~ (g `GenericAp` x)
+
+class PApplicative f where
+  type Pure (x :: a) :: f a
+  type Pure x = GenericPure x
+
+  type (g :: f (a ~> b)) <*> (x :: f a) :: f b
+  type g <*> x = g `GenericAp` x
+
+data PureSym0 :: forall f a. a ~> f a
+type instance Apply PureSym0 x = Pure x
+
+data (<*>@#@$) :: forall f a b. f (a ~> b) ~> f a ~> f b
+type instance Apply (<*>@#@$) g = (<*>@#@$$) g
+data (<*>@#@$$) :: forall f a b. f (a ~> b) -> f a ~> f b
+type instance Apply ((<*>@#@$$) g) x = g <*> x
+
+class SApplicative f where
+  sPure         :: forall a (x :: a).
+                   Sing x -> Sing (Pure x :: f a)
+  default sPure :: forall a (x :: a).
+                   ( SGeneric1 f, SApplicative (Rep1 f)
+                   , GenericPureC f x )
+                => Sing x -> Sing (Pure x :: f a)
+  sPure = sTo1 . sPure
+
+  (%<*>)         :: forall a b (g :: f (a ~> b)) (x :: f a).
+                    Sing g -> Sing x -> Sing (g <*> x)
+  default (%<*>) :: forall a b (g :: f (a ~> b)) (x :: f a).
+                    ( SGeneric1 f, SApplicative (Rep1 f)
+                    , GenericApC g x )
+                 => Sing g -> Sing x -> Sing (g <*> x)
+  sg %<*> sx = sTo1 (sFrom1 sg %<*> sFrom1 sx)
+
+class (PApplicative f, SApplicative f) => VApplicative f where
+  applicativeHomomorphism         :: forall a b (g :: a ~> b) (x :: a).
+                                     Sing g -> Sing x
+                                  -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
+  default applicativeHomomorphism :: forall a b (g :: a ~> b) (x :: a).
+                                     ( VGeneric1 f, VApplicative (Rep1 f)
+                                     , GenericPureC f g, GenericPureC f x, GenericPureC f (g `Apply` x)
+                                     , GenericApC (Pure g :: f (a ~> b)) (Pure x :: f a)
+                                     )
+                                  => Sing g -> Sing x
+                                  -> (Pure g <*> Pure x) :~: (Pure (g `Apply` x) :: f b)
+  applicativeHomomorphism sg sx
+    | Refl <- sFot1 @Type @f (sPure sg)
+    , Refl <- sFot1 @Type @f (sPure sx)
+    , Refl <- applicativeHomomorphism @(Rep1 f) sg sx
+    , Refl <- sFot1 @Type @f pureGX
+    , Refl <- sTof1 @Type @f (sTo1 pureGX)
+    = Refl
+    where
+      pureGX :: Sing (Pure (Apply g x) :: Rep1 f b)
+      pureGX = sPure (sg @@ sx)
+
+instance PApplicative (K1 i c) where
+  type Pure _ = 'K1 Mempty
+  type 'K1 x <*> 'K1 y = 'K1 (x <> y)
+
+instance SMonoid c => SApplicative (K1 i c) where
+  sPure _ = SK1 sMempty
+  SK1 x %<*> SK1 y = SK1 (x %<> y)
+
+instance VMonoid c => VApplicative (K1 i c) where
+  applicativeHomomorphism _ _ | Refl <- monoidLeftIdentity (sMempty @c) = Refl
+
+instance PApplicative (M1 i c f) where
+  type Pure x = 'M1 (Pure x)
+  type 'M1 ff <*> 'M1 x = 'M1 (ff <*> x)
+
+instance VApplicative f => VApplicative (M1 i c f) where
+  applicativeHomomorphism sg sx
+    | Refl <- applicativeHomomorphism @f sg sx
+    = Refl
+
+instance PApplicative (f :*: g) where
+  type Pure a = Pure a ':*: Pure a
+  type (ff ':*: gg) <*> (x ':*: y) = (ff <*> x) ':*: (gg <*> y)
+
+instance (SApplicative f, SApplicative g) => SApplicative (f :*: g) where
+  sPure a = sPure a :%*: sPure a
+  (f :%*: g) %<*> (x :%*: y) = (f %<*> x) :%*: (g %<*> y)
+
+instance (VApplicative f, VApplicative g) => VApplicative (f :*: g) where
+  applicativeHomomorphism sg sx
+    | Refl <- applicativeHomomorphism @f sg sx
+    , Refl <- applicativeHomomorphism @g sg sx
+    = Refl
+
+instance PApplicative Par1 where
+  type Pure x = 'Par1 x
+  type 'Par1 f <*> 'Par1 x = 'Par1 (f @@ x)
+
+instance SApplicative Par1 where
+  sPure = SPar1
+  SPar1 f %<*> SPar1 x = SPar1 (f @@ x)
+
+instance VApplicative Par1 where
+  applicativeHomomorphism _ _ = Refl
diff --git a/testsuite/tests/perf/compiler/T15703_aux.hs b/testsuite/tests/perf/compiler/T15703_aux.hs
new file mode 100644
index 0000000000..866eb3b9d4
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T15703_aux.hs
@@ -0,0 +1,139 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE InstanceSigs #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+module T15703_aux where
+
+import Data.Kind
+import Data.Type.Equality
+import GHC.Generics
+
+data family Sing :: forall k. k -> Type
+data instance Sing :: forall a b. (a, b) -> Type where
+  STuple2 :: Sing x -> Sing y -> Sing '(x, y)
+
+data TyFun :: Type -> Type -> Type
+type a ~> b = TyFun a b -> Type
+infixr 0 ~>
+type family Apply (f :: k1 ~> k2) (x :: k1) :: k2
+type f @@ x = f `Apply` x
+infixl 9 @@
+
+newtype instance Sing (f :: k1 ~> k2) =
+  SLambda { applySing :: forall t. Sing t -> Sing (f @@ t) }
+
+type SingFunction1 f = forall t. Sing t -> Sing (f @@ t)
+singFun1 :: forall f. SingFunction1 f -> Sing f
+singFun1 f = SLambda f
+
+type SingFunction2 (f :: a1 ~> a2 ~> b) =
+  forall t1 t2. Sing t1 -> Sing t2 -> Sing (f @@ t1 @@ t2)
+singFun2 :: forall f. SingFunction2 f -> Sing f
+singFun2 f = SLambda (\x -> singFun1 (f x))
+
+type SingFunction3 (f :: a1 ~> a2 ~> a3 ~> b) =
+     forall t1 t2 t3.
+     Sing t1 -> Sing t2 -> Sing t3
+  -> Sing (f @@ t1 @@ t2 @@ t3)
+singFun3 :: forall f. SingFunction3 f -> Sing f
+singFun3 f = SLambda (\x -> singFun2 (f x))
+
+(@@) :: forall k1 k2 (f :: k1 ~> k2) (t :: k1). Sing f -> Sing t -> Sing (f @@ t)
+(@@) f = applySing f
+
+type family ((f :: b ~> c) :. (g :: a ~> b)) (x :: a) :: c where
+  (f :. g) x = f @@ (g @@ x)
+
+data (.@#@$) :: forall b c a. (b ~> c) ~> (a ~> b) ~> (a ~> c)
+type instance Apply (.@#@$) f = (.@#@$$) f
+data (.@#@$$) :: forall b c a. (b ~> c) -> (a ~> b) ~> (a ~> c)
+type instance Apply ((.@#@$$) f) g = f .@#@$$$ g
+data (.@#@$$$) :: forall b c a. (b ~> c) -> (a ~> b) -> (a ~> c)
+type instance Apply (f .@#@$$$ g) x = (f :. g) x
+
+(%.) :: forall b c a (f :: b ~> c) (g :: a ~> b) (x :: a).
+        Sing f -> Sing g -> Sing x -> Sing ((f :. g) x)
+(f %. g) x = f @@ (g @@ x)
+
+type family Id (x :: a) :: a where
+  Id x = x
+
+data IdSym0 :: forall a. a ~> a
+type instance Apply IdSym0 x = Id x
+
+sId :: forall a (x :: a). Sing x -> Sing (Id x)
+sId x = x
+
+data instance Sing :: forall i k c (p :: k). K1 i c p -> Type where
+  SK1 :: Sing x -> Sing ('K1 x)
+
+data instance Sing :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
+                      M1 i c f p -> Type where
+  SM1 :: Sing x -> Sing ('M1 x)
+data M1Sym0 :: forall k i (c :: Meta) (f :: k -> Type) (p :: k).
+               f p ~> M1 i c f p
+type instance Apply M1Sym0 x = 'M1 x
+
+data instance Sing :: forall k (f :: k -> Type) (g :: k -> Type) (p :: k).
+                      (f :*: g) p -> Type where
+  (:%*:) :: Sing x -> Sing y -> Sing (x ':*: y)
+
+data instance Sing :: forall p. Par1 p -> Type where
+  SPar1 :: Sing x -> Sing ('Par1 x)
+
+class PGeneric1 (f :: k -> Type) where
+  type From1 (z :: f a)      :: Rep1 f a
+  type To1   (z :: Rep1 f a) :: f a
+
+class SGeneric1 (f :: k -> Type) where
+  sFrom1 :: forall (a :: k) (z :: f a).      Sing z -> Sing (From1 z)
+  sTo1   :: forall (a :: k) (r :: Rep1 f a). Sing r -> Sing (To1 r :: f a)
+
+class (PGeneric1 f, SGeneric1 f) => VGeneric1 (f :: k -> Type) where
+  sTof1 :: forall (a :: k) (z :: f a).      Sing z -> To1 (From1 z)        :~: z
+  sFot1 :: forall (a :: k) (r :: Rep1 f a). Sing r -> From1 (To1 r :: f a) :~: r
+
+instance PGeneric1 ((,) a) where
+  type From1 '(x, y) = 'M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))
+  type To1   ('M1 ('M1 ('M1 ('K1 x) ':*: 'M1 ('Par1 y)))) = '(x, y)
+
+instance SGeneric1 ((,) a) where
+  sFrom1 (STuple2 x y) = SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))
+  sTo1   (SM1 (SM1 (SM1 (SK1 x) :%*: SM1 (SPar1 y)))) = STuple2 x y
+
+instance VGeneric1 ((,) a) where
+  sTof1 STuple2{} = Refl
+  sFot1 (SM1 (SM1 (SM1 SK1{} :%*: SM1 SPar1{}))) = Refl
+
+class PSemigroup a where
+  type (x :: a) <> (y :: a) :: a
+
+class SSemigroup a where
+  (%<>) :: forall (x :: a) (y :: a).
+           Sing x -> Sing y -> Sing (x <> y)
+
+class (PSemigroup a, SSemigroup a) => VSemigroup a where
+  semigroupAssociative :: forall (x :: a) (y :: a) (z :: a).
+                          Sing x -> Sing y -> Sing z
+                       -> (x <> (y <> z)) :~: ((x <> y) <> z)
+
+class PSemigroup a => PMonoid a where
+  type Mempty :: a
+
+class SSemigroup a => SMonoid a where
+  sMempty :: Sing (Mempty :: a)
+
+class (PMonoid a, SMonoid a, VSemigroup a) => VMonoid a where
+  monoidLeftIdentity  :: forall (x :: a).
+                         Sing x -> (Mempty <> x) :~: x
+  monoidRightIdentity :: forall (x :: a).
+                         Sing x -> (x <> Mempty) :~: x
diff --git a/testsuite/tests/perf/compiler/T8095.hs b/testsuite/tests/perf/compiler/T8095.hs
new file mode 100644
index 0000000000..8d0c8c3e08
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T8095.hs
@@ -0,0 +1,19 @@
+{-# OPTIONS_GHC -freduction-depth=1000 #-}
+{-# LANGUAGE TypeOperators,DataKinds,KindSignatures,TypeFamilies,PolyKinds,UndecidableInstances #-}
+import GHC.TypeLits
+data Nat1 = Zero | Succ Nat1
+type family Replicate1 (n :: Nat1) (x::a) :: [a]
+type instance Replicate1 n x = Replicate1' '[] n x
+type family Replicate1' (acc::[a]) (n :: Nat1) (x::a)  :: [a]
+type instance Replicate1' acc Zero x = acc
+type instance Replicate1' acc (Succ n) x = Replicate1' (x ': acc) n x
+class Class a where
+    f :: a -> a
+data Data (xs::a) = X | Y
+    deriving (Read,Show)
+main = print test1
+instance (xs ~ Replicate1 ( Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) ()) => Class (Data xs) where
+    f X = Y
+    f Y = X
+test1 = f (X :: Data ( Replicate1 ( Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Succ (  Zero ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))) () ))
+
diff --git a/testsuite/tests/perf/compiler/T9872b_defer.hs b/testsuite/tests/perf/compiler/T9872b_defer.hs
new file mode 100644
index 0000000000..eaa6afb142
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T9872b_defer.hs
@@ -0,0 +1,115 @@
+{-
+ - Instant Insanity using Closed Type Families and DataKinds.
+ -
+ - See:  http://stackoverflow.com/questions/26538595
+ -}
+
+{-# OPTIONS_GHC -freduction-depth=400 #-}
+
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE DataKinds, KindSignatures, PolyKinds #-}
+{-# LANGUAGE TypeOperators #-}
+
+import Prelude hiding (all, flip, map, filter )
+
+data Proxy (a :: k) = Proxy
+
+main = print (Proxy :: Proxy (Solutions Cubes))
+
+data Color = R | G | B | W
+
+data Cube = Cube Color Color Color Color Color Color
+
+type family And (b1 :: Bool) (b2 :: Bool) :: Bool where
+    And True True = True
+    And b1 b2 = False
+
+type family NE (x :: Color) (y :: Color) :: Bool where
+    NE x x = False
+    NE x y = True
+
+type family EQ (x :: Color) (y :: Color) :: Bool where
+    EQ a a = True
+    EQ a b = False
+
+type family All (l :: [Bool]) :: Bool where
+    All '[] = True
+    All (False ': xs) = False
+    All (True ': xs) = All xs
+
+type family ListConcat (xs :: [k]) (ys :: [k]) :: [k] where
+    ListConcat '[] ys = ys
+    ListConcat (x ': xs) ys = x ': ListConcat xs ys
+
+type family AppendIf (b :: Bool) (a :: [Cube]) (as :: [[Cube]]) :: [[Cube]] where
+    AppendIf False a as = as
+    AppendIf True a as = a ': as
+
+data Transform = Rotate | Twist | Flip
+
+type family Apply (f :: Transform) (a :: Cube) :: Cube where
+    Apply Rotate ('Cube u f r b l d) = ('Cube u r b l f d)
+    Apply Twist  ('Cube u f r b l d) = ('Cube f r u l d b)
+    Apply Flip   ('Cube u f r b l d) = ('Cube d l b r f u)
+
+type family Map (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Map f '[] = '[]
+    Map f (a ': as) = (Apply f a) ': (Map f as)
+
+type family MapAppend (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend f xs = ListConcat xs (Map f xs)
+
+type family MapAppend2 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend2 f xs = ListConcat xs (MapAppend f (Map f xs))
+
+type family MapAppend3 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    MapAppend3 f xs = ListConcat xs (MapAppend2 f (Map f xs))
+
+type family Iterate2 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate2 f '[] = '[]
+    Iterate2 f (a ': as) = ListConcat [Apply f a, a] (Iterate2 f as)
+
+type family Iterate3 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate3 f '[] = '[]
+    Iterate3 f (a ': as) =
+        ListConcat [a, Apply f a, Apply f (Apply f a)] (Iterate3 f as)
+
+type family Iterate4 (f :: Transform) (as :: [Cube]) :: [Cube] where
+    Iterate4 f '[] = '[]
+    Iterate4 f (a ': as) =
+        ListConcat [a, Apply f a, Apply f (Apply f a), Apply f (Apply f (Apply f a))]
+                   (Iterate4 f as)
+
+type family Orientations (c :: Cube) :: [Cube] where
+    Orientations c = MapAppend3 Rotate (MapAppend2 Twist (MapAppend Flip '[c]))
+
+type Cube1 = 'Cube B G W G B R
+type Cube2 = 'Cube W G B W R R
+type Cube3 = 'Cube G W R B R R
+type Cube4 = 'Cube B R G G W W
+
+type Cubes = [Cube1, Cube2, Cube3, Cube4]
+
+type family Compatible (c :: Cube) (d :: Cube) :: Bool where
+    Compatible ('Cube u1 f1 r1 b1 l1 d1) ('Cube u2 f2 r2 b2 l2 d2) =
+        All [NE f1 f2, NE r1 r2, NE b1 b2, NE l1 l2]
+
+type family Allowed (c :: Cube) (cs :: [Cube]) :: Bool where
+    Allowed c '[] = True
+    Allowed c (s ': ss) = And (Compatible c s) (Allowed c ss)
+
+type family MatchingOrientations (as :: [Cube]) (sol :: [Cube]) :: [[Cube]] where
+    MatchingOrientations '[] sol = '[]
+    MatchingOrientations (o ': os) sol =
+        AppendIf (Allowed o sol) (o ': sol) (MatchingOrientations os sol)
+
+type family AllowedCombinations (os :: [Cube]) (sols :: [[Cube]]) where
+    AllowedCombinations os '[] = '[]
+    AllowedCombinations os (sol ': sols) =
+        ListConcat (MatchingOrientations os sol) (AllowedCombinations os sols)
+
+type family Solutions (cs :: [Cube]) :: [[Cube]] where
+    Solutions '[] = '[ '[] ]
+    Solutions (c ': cs) = AllowedCombinations (Orientations c) (Solutions cs)
diff --git a/testsuite/tests/perf/compiler/T9872b_defer.stderr b/testsuite/tests/perf/compiler/T9872b_defer.stderr
new file mode 100644
index 0000000000..965f9e0c43
--- /dev/null
+++ b/testsuite/tests/perf/compiler/T9872b_defer.stderr
@@ -0,0 +1,24 @@
+
+T9872b_defer.hs:19:8: warning: [-Wdeferred-type-errors (in -Wdefault)]
+    • No instance for (Show
+                         (Proxy
+                            '[ '[ 'Cube 'G 'B 'W 'R 'B 'G, 'Cube 'W 'G 'B 'W 'R 'R,
+                                  'Cube 'R 'W 'R 'B 'G 'R, 'Cube 'B 'R 'G 'G 'W 'W],
+                               '[ 'Cube 'G 'B 'R 'W 'B 'G, 'Cube 'R 'R 'W 'B 'G 'W,
+                                  'Cube 'R 'G 'B 'R 'W 'R, 'Cube 'W 'W 'G 'G 'R 'B],
+                               '[ 'Cube 'G 'W 'R 'B 'B 'G, 'Cube 'W 'B 'W 'R 'G 'R,
+                                  'Cube 'R 'R 'B 'G 'W 'R, 'Cube 'B 'G 'G 'W 'R 'W],
+                               '[ 'Cube 'G 'R 'W 'B 'B 'G, 'Cube 'R 'W 'B 'G 'R 'W,
+                                  'Cube 'R 'B 'R 'W 'G 'R, 'Cube 'W 'G 'G 'R 'W 'B],
+                               '[ 'Cube 'G 'R 'B 'B 'W 'G, 'Cube 'W 'W 'R 'G 'B 'R,
+                                  'Cube 'R 'B 'G 'W 'R 'R, 'Cube 'B 'G 'W 'R 'G 'W],
+                               '[ 'Cube 'G 'W 'B 'B 'R 'G, 'Cube 'R 'B 'G 'R 'W 'W,
+                                  'Cube 'R 'R 'W 'G 'B 'R, 'Cube 'W 'G 'R 'W 'G 'B],
+                               '[ 'Cube 'G 'B 'B 'W 'R 'G, 'Cube 'W 'R 'G 'B 'W 'R,
+                                  'Cube 'R 'G 'W 'R 'B 'R, 'Cube 'B 'W 'R 'G 'G 'W],
+                               '[ 'Cube 'G 'B 'B 'R 'W 'G, 'Cube 'R 'G 'R 'W 'B 'W,
+                                  'Cube 'R 'W 'G 'B 'R 'R, 'Cube 'W 'R 'W 'G 'G 'B]]))
+        arising from a use of ‘print’
+    • In the expression: print (Proxy :: Proxy (Solutions Cubes))
+      In an equation for ‘main’:
+          main = print (Proxy :: Proxy (Solutions Cubes))
diff --git a/testsuite/tests/perf/compiler/all.T b/testsuite/tests/perf/compiler/all.T
index 532db501e6..6327b8cc0a 100644
--- a/testsuite/tests/perf/compiler/all.T
+++ b/testsuite/tests/perf/compiler/all.T
@@ -145,6 +145,13 @@ test('T9872b',
       ],
      compile_fail,
      [''])
+test('T9872b_defer',
+     [ only_ways(['normal']),
+       collect_compiler_stats('bytes allocated', 1),
+       high_memory_usage
+      ],
+     compile,
+     ['-fdefer-type-errors'])
 test('T9872c',
      [ only_ways(['normal']),
        collect_compiler_stats('bytes allocated', 1),
@@ -158,6 +165,30 @@ test('T9872d',
       ],
      compile,
      [''])
+test ('T8095',
+      [ only_ways(['normal']),
+        collect_compiler_stats('bytes allocated',1) ],
+      compile,
+      ['-v0 -O'])
+test ('T13386',
+      [ only_ways(['normal']),
+        collect_compiler_stats('bytes allocated',1) ],
+      compile,
+      ['-v0 -O0'])
+test ('T15703',
+      [ only_ways(['normal']),
+        collect_compiler_stats('bytes allocated',1)
+      , extra_files(['T15703_aux.hs'])
+      ],
+      multimod_compile,
+      ['T15703', '-v0 -O'])
+test ('LargeRecord',
+      [ only_ways(['normal']),
+        collect_compiler_stats('bytes allocated',1)
+      , extra_files(['SuperRecord.hs'])
+      ],
+      multimod_compile,
+      ['LargeRecord', '-v0 -O'])
 
 test('T9961',
      [ only_ways(['normal']),