diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,5 @@
+# Revision history for coercion-check
+
+## 0.1.0.0 -- YYYY-mm-dd
+
+* First version. Released on an unsuspecting world.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Jonathan Lorimer and Sandy Maguire (c) 2021
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+ * Redistributions of source code must retain the above copyright
+ notice, this list of conditions and the following disclaimer.
+
+ * Redistributions in binary form must reproduce the above
+ copyright notice, this list of conditions and the following
+ disclaimer in the documentation and/or other materials provided
+ with the distribution.
+
+ * Neither the name of Sandy Maguire nor the names of other
+ contributors may be used to endorse or promote products derived
+ from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,86 @@
+ Core Warn
+
+
+ 
+
+
+ 
+
+
+ 
+
+
+
+## Motivation
+
+This plugin was inspired by these two blog posts from [Well
+Typed](https://well-typed.com/): [part
+1](https://well-typed.com/blog/2021/08/large-records/), [part
+2](https://well-typed.com/blog/2021/10/large-records-part-2/). They discuss two
+scenarios where GHC's core representation deviates drastically from what one
+might expect. These phenomena can be grouped into two buckets: instances where
+GHC produces too many unnecessary type coercions, and instances where GHC
+produces large chains of dictionary references. The first can be solved by
+ensuring that all expensive instances occur in a phantom context, and the
+second can be solved by ensuring that all inductive instances are balanced.
+
+## Usage
+
+### Stack
+
+In your `stack.yaml` add this
+
+```yaml
+extra-deps:
+- core-warn-0.1.0.0
+```
+
+and then in `package.yaml` add:
+
+```yaml
+dependencies:
+- core-warn
+
+ghc-options:
+- -fplugin=CoreWarn
+```
+
+### Cabal
+
+Add these lines to the corresponding stanza of your cabal file. For example if
+you want to run `CoreWarn` on your library stanza, add the below code block as
+a child of `library`.
+
+```cabal
+ghc-options: -fplugin=CoreWarn
+build-depends: base >=4.10 && <5
+ , ...
+ , core-warn
+```
+
+or you can run this option from the command line for a specific component, in
+this example we chose the `test` component:
+
+```shell
+$ cabal repl test --ghc-options=-fplugin=CoreWarn
+```
+
+### Options
+
+Here is an example of how you would apply an option to this plugin. For the
+sake of variety we will use a file level pragma as the example.
+
+```haskell
+{-# OPTIONS_GHC -fplugin-opt=CoreWarn: #-}
+```
+
+The plugin accepts four arguments, but by default opts in. For example if you
+wanted to only show warning for one kind of issue mentioned above, you could
+use the follwing options:
+ - `warn-large-coercions`
+ - `warn-deep-dicts`
+
+If you have `CoreWarn` enabled for the entire project, you might want to disable it
+in a particular file. You can do so with the following options:
+ - `no-warn-large-coercions`
+ - `no-warn-deep-dicts`
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/core-warn.cabal b/core-warn.cabal
new file mode 100644
--- /dev/null
+++ b/core-warn.cabal
@@ -0,0 +1,57 @@
+cabal-version: >=1.10
+-- Initial package description 'coercion-check.cabal' generated by 'cabal
+-- init'. For further documentation, see
+-- http://haskell.org/cabal/users-guide/
+
+name: core-warn
+version: 0.1.0.0
+author: Jonathan Lorimer
+maintainer: jonathan_lorimer@mac.com
+build-type: Simple
+extra-source-files: CHANGELOG.md, README.md
+category: Warning
+synopsis: "Provide warnings for unexpected Core generation"
+description: Please see the README on GitHub at
+license: BSD3
+license-file: LICENSE
+
+
+library
+ exposed-modules: CoreWarn
+ other-modules: Warn.Coercion
+ , Warn.Dictionary
+ ghc-options: -Wall
+ build-depends: base >=4.10 && <5
+ , ghc
+ , syb
+ , containers
+ , containers-good-graph
+ hs-source-dirs: src
+ default-extensions: RecordWildCards
+ , LambdaCase
+ , BlockArguments
+ , ScopedTypeVariables
+ , ConstraintKinds
+ , DataKinds
+ , FlexibleContexts
+ , FlexibleInstances
+ , GADTs
+ , LambdaCase
+ , MultiParamTypeClasses
+ , PolyKinds
+ , RankNTypes
+ , DerivingStrategies
+ , TypeApplications
+
+ default-language: Haskell2010
+
+test-suite test
+ default-extensions: TypeApplications, DataKinds, PolyKinds, TypeOperators, TypeFamilies, UndecidableInstances
+ type: exitcode-stdio-1.0
+ main-is: Main.hs
+ other-modules: Spec, Infra, GoodTest, BadTest, InductionTest
+ ghc-options: -fplugin=CoreWarn
+ hs-source-dirs: test
+ build-depends: base >=4.10 && <5
+ , core-warn
+ default-language: Haskell2010
diff --git a/src/CoreWarn.hs b/src/CoreWarn.hs
new file mode 100644
--- /dev/null
+++ b/src/CoreWarn.hs
@@ -0,0 +1,220 @@
+{-# LANGUAGE CPP #-}
+
+#if __GLASGOW_HASKELL__ >= 810
+#define REASON NoReason
+#else
+#define REASON
+#endif
+
+#if __GLASGOW_HASKELL__ >= 900
+#define VARBINDARG
+#else
+#define VARBINDARG _
+#endif
+
+module CoreWarn (plugin) where
+
+import Warn.Coercion
+import Warn.Dictionary
+import Control.Monad
+import Data.Bool (bool)
+import Data.Foldable
+import Data.Graph.Good
+import Data.IORef
+import Data.Maybe (fromMaybe)
+import Data.Monoid
+import GHC (GhcTc)
+import Generics.SYB
+import Prelude hiding (lookup)
+import System.IO.Unsafe (unsafePerformIO)
+import qualified Data.Map as M
+import qualified Data.Set as S
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Core.Stats
+import GHC.Plugins hiding (typeSize, (<>))
+import GHC.Tc.Types (tcg_binds)
+import Data.List (nub)
+#else
+import Data.Containers.ListUtils (nubOrd)
+import CoreStats
+import GhcPlugins hiding (typeSize, (<>))
+import TcRnMonad (tcg_binds)
+#endif
+
+#if __GLASGOW_HASKELL__ >= 810
+import GHC.Hs.Expr
+import GHC.Hs.Binds
+#else
+import HsExpr
+import HsBinds
+#endif
+
+------------------------------------------------------------------------------
+-- | The main @core-warn@ program.
+plugin :: Plugin
+plugin =
+ defaultPlugin
+ { installCoreToDos = \ss ctds -> do
+ binds <- liftIO $ readIORef global_tcg_ref
+ pure $ ctds ++ [coreWarn (parseOpts ss) binds]
+ , pluginRecompile = const $ pure NoForceRecompile
+ , typeCheckResultAction = \_ _ tcg -> do
+ liftIO $ writeIORef global_tcg_ref $ tcg_binds tcg
+ pure tcg
+ }
+
+
+------------------------------------------------------------------------------
+-- | We need to get our grubby little hands on the 'tcg_binds', but the
+-- core-to-core plugin interface doesn't give us access to them. So we do this
+-- very safe trick to get a hold of them.
+global_tcg_ref :: IORef (LHsBinds GhcTc)
+global_tcg_ref = unsafePerformIO $ newIORef $ error "no tcg_binds set"
+{-# NOINLINE global_tcg_ref #-}
+
+
+------------------------------------------------------------------------------
+-- | Options for @core-warn@. These are opt-out.
+data CoreWarnOpts = CoreWarnOpts
+ { cwo_warnBigCoerces :: Endo Bool,
+ cwo_warnDeepDicts :: Endo Bool
+ }
+
+instance Semigroup CoreWarnOpts where
+ (<>) (CoreWarnOpts lb4 lb5) (CoreWarnOpts lb lb3) =
+ CoreWarnOpts
+ { cwo_warnBigCoerces = lb <> lb4,
+ cwo_warnDeepDicts = lb3 <> lb5
+ }
+
+instance Monoid CoreWarnOpts where
+ mempty =
+ CoreWarnOpts
+ { cwo_warnBigCoerces = mempty,
+ cwo_warnDeepDicts = mempty
+ }
+
+
+------------------------------------------------------------------------------
+-- | Parse options.
+parseOpts :: [CommandLineOption] -> CoreWarnOpts
+parseOpts = go
+ where
+ go = foldMap $ \case
+ "warn-large-coercions" -> CoreWarnOpts (Endo $ pure True) mempty
+ "no-warn-large-coercions" -> CoreWarnOpts (Endo $ pure False) mempty
+ "warn-deep-dicts" -> CoreWarnOpts mempty (Endo $ pure True)
+ "no-warn-deep-dicts" -> CoreWarnOpts mempty (Endo $ pure False)
+ _ -> mempty
+
+
+------------------------------------------------------------------------------
+-- | Given an 'OccName' corresponding to a dictionary, find every immediate
+-- 'SrcSpan's that contain it.
+findDictRef :: Data a => OccName -> a -> [SrcSpan]
+findDictRef occ = everything (<>) $ mkQ mempty $ \case
+#if __GLASGOW_HASKELL__ >= 900
+ L loc (XExpr (WrapExpr ev))
+#else
+ L loc (HsWrap _ ev _)
+#endif
+ | isGoodSrcSpan loc ->
+ everything (<>)
+ (mkQ mempty $ \(v :: Var) -> bool [] [loc] $ getOccName v == occ)
+ ev
+ (_ :: LHsExpr GhcTc) -> []
+
+
+------------------------------------------------------------------------------
+-- | Given an 'OccName', find the src span for every coercion inside of its
+-- definition.
+findBindCoercions :: Data a => Name -> a -> [SrcSpan]
+findBindCoercions occ = everything (<>) $ mkQ mempty $ \case
+ x@(VarBind _ a _ VARBINDARG)
+ | getName a == occ ->
+ get_sub x
+ x@(FunBind _ (L _ a) _ _ VARBINDARG)
+ | getName a == occ ->
+ get_sub x
+ x@(AbsBinds _ _ b e _ _ _)
+ | any ((== occ) . getName) b
+ || any ((== occ) . getName . abe_poly) e -> get_sub x
+ (_ :: HsBindLR GhcTc GhcTc) -> []
+ where
+ get_sub x =
+ everything (<>) (mkQ mempty $ \case
+#if __GLASGOW_HASKELL__ >= 900
+ L loc (XExpr (WrapExpr y))
+#else
+ L loc (HsWrap _ y _)
+#endif
+ | isGoodSrcSpan loc
+ , gtypecount (undefined :: Coercion) y > 0 -> [loc]
+ (_ :: LHsExpr GhcTc) -> []
+ ) x
+
+
+------------------------------------------------------------------------------
+-- | Like 'fromMaybe' but for lists.
+singletonIfEmpty :: a -> [a] -> [a]
+singletonIfEmpty a as = if null as then [a] else as
+
+
+------------------------------------------------------------------------------
+-- | Is this 'CoreBndr' the 'Var' of a dictionary?
+isDictVar :: CoreBndr -> Bool
+isDictVar bndr = fromMaybe False $ do
+ (tycon, _) <- tcSplitTyConApp_maybe $ idType bndr
+ _cls <- tyConClass_maybe tycon
+ pure True
+
+
+------------------------------------------------------------------------------
+-- | Translatea @'Bind' 'CoreBndr'@ into a map from 'CoreBndr's to 'CoreExpr's.
+coreBndrToExprMap :: Bind CoreBndr -> M.Map CoreBndr CoreExpr
+coreBndrToExprMap (NonRec var ex) = M.singleton var ex
+coreBndrToExprMap (Rec ex) = foldMap (uncurry M.singleton) ex
+
+
+------------------------------------------------------------------------------
+-- | The @core-warn@ todo pass.
+coreWarn :: CoreWarnOpts -> LHsBinds GhcTc -> CoreToDo
+coreWarn opts binds = CoreDoPluginPass "coercionCheck" $ \guts -> do
+ let programMap = foldMap coreBndrToExprMap $ mg_binds guts
+ dictSets = fmap (S.fromList . toList)
+ . components
+ . graphFromEdges
+ . filter (isDictVar . fst)
+ . M.toList . fmap S.toList
+ . mkCoreAdjacencyMap
+ $ programMap
+
+ when (flip appEndo True $ cwo_warnDeepDicts opts) $
+ for_ dictSets \dictSet -> do
+ let srcSpans
+ = filter isGoodSrcSpan
+ $ foldMap (flip findDictRef binds)
+ $ foldMap (S.singleton . occName) dictSet
+ when (shouldWarnDeepDict dictSet) $
+ warnMsg REASON $
+ pprDeepDict srcSpans dictSet
+
+ when (flip appEndo True $ cwo_warnBigCoerces opts) $
+ for_ (M.toList . fmap exprStats $ programMap) \(coreBndr, coreStats) ->
+ when (shouldWarnLargeCoercion coreStats) $
+ warnMsg REASON $
+ pprWarnLargeCoerce
+ (singletonIfEmpty noSrcSpan $
+#if __GLASGOW_HASKELL__ >= 900
+ -- TODO(sandy): I know it's slow, but blame GHC9 for getting rid
+ -- of the 'Ord' instance on 'SrcSpan
+ nub
+#else
+ nubOrd
+#endif
+ $ findBindCoercions (getName coreBndr) binds)
+ coreBndr
+ coreStats
+ pure guts
+
diff --git a/src/Warn/Coercion.hs b/src/Warn/Coercion.hs
new file mode 100644
--- /dev/null
+++ b/src/Warn/Coercion.hs
@@ -0,0 +1,50 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE NamedFieldPuns #-}
+
+module Warn.Coercion where
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Core.Stats
+import GHC.Plugins hiding ((<>))
+import GHC.Utils.Ppr.Colour
+#else
+import CoreStats
+import GhcPlugins hiding ((<>))
+import PprColour
+#endif
+
+------------------------------------------------------------------------------
+-- | Pretty print a "large number of coercions" warning.
+pprWarnLargeCoerce :: [SrcSpan] -> CoreBndr -> CoreStats -> SDoc
+pprWarnLargeCoerce refs bind stats =
+ let srcSpanList = if length refs >= 3
+ then take 3 ((bullet <+>) . ppr <$> refs) <> [text "..."]
+ else (bullet <+>) . ppr <$> refs
+ CS{..} = stats
+ in vcat [ text "Found a large number of coercions in GHC Core."
+ , nest 2 $ text " GHC produced a a quadratic number of coercions relative to the number of terms."
+ $$ text "This can happen for expensive type families that are used outside of phantom contexts."
+ , blankLine
+ , hsep [ text "These coercions were introduced in"
+ , coloured colBlueFg . ppr . getOccName $ bind
+ , text "at these locations:"
+ ]
+ , nest 4 (vcat srcSpanList)
+ , blankLine
+ , sep [ text "Terms:", coloured colBlueFg $ ppr cs_tm
+ , text "Types:", coloured colBlueFg $ ppr cs_ty
+ , text "Coercions:", coloured colBlueFg $ ppr cs_co
+ ]
+ , text ""
+ ]
+
+
+------------------------------------------------------------------------------
+-- | Heuristic for whether we should show a "large number of coercions"
+-- warning.
+shouldWarnLargeCoercion :: CoreStats -> Bool
+shouldWarnLargeCoercion CS {cs_tm, cs_co} =
+ let quad = cs_tm * floor (logBase @Double 2 $ fromIntegral cs_tm)
+ in cs_co >= quad && cs_co > 100
+
+
diff --git a/src/Warn/Dictionary.hs b/src/Warn/Dictionary.hs
new file mode 100644
--- /dev/null
+++ b/src/Warn/Dictionary.hs
@@ -0,0 +1,105 @@
+{-# LANGUAGE CPP #-}
+
+#if __GLASGOW_HASKELL__ >= 900
+#define FUNTYARG _ _
+#elif __GLASGOW_HASKELL__ == 810
+#define FUNTYARG _
+#else
+#define FUNTYARG
+#endif
+
+module Warn.Dictionary where
+
+import Data.Foldable
+import Data.Generics.Aliases
+import Data.Generics.Schemes
+import Data.Map (Map)
+import Data.Ord
+import Data.Set (Set)
+import qualified Data.Set as Set
+
+#if __GLASGOW_HASKELL__ >= 900
+import GHC.Plugins hiding ((<>))
+import GHC.Tc.Utils.TcType (tcSplitNestedSigmaTys)
+import GHC.Core.TyCo.Rep
+import GHC.Utils.Ppr.Colour
+#else
+import GhcPlugins hiding ((<>))
+import TcType (tcSplitNestedSigmaTys)
+import TyCoRep
+import PprColour
+#endif
+
+
+------------------------------------------------------------------------------
+-- | Build an adjacency map from core bindings to the core bindings they
+-- reference.
+mkCoreAdjacencyMap :: Map CoreBndr CoreExpr -> Map CoreBndr (Set CoreBndr)
+mkCoreAdjacencyMap = fmap $ everything mappend (mkQ mempty Set.singleton)
+
+
+------------------------------------------------------------------------------
+-- | Get the biggest type (via 'typeSizeWithoutKinds') in a set.
+biggestType :: Set CoreBndr -> Type
+biggestType = rhsType . idType . maximumBy (comparing (typeSizeWithoutKinds . rhsType . idType))
+
+
+------------------------------------------------------------------------------
+-- | Remove the forall quantifiers and contexts from a type.
+rhsType :: Type -> Type
+rhsType ty =
+ case tcSplitNestedSigmaTys ty of
+ (_, _, ty') -> ty'
+
+
+------------------------------------------------------------------------------
+-- | Heuristic for whether we should show the "deep dicts" warning.
+shouldWarnDeepDict :: Set CoreBndr -> Bool
+shouldWarnDeepDict coreBndrs =
+ let amountOfCoreBndrs = Set.size coreBndrs
+ biggestTypeSize = typeSizeWithoutKinds (biggestType coreBndrs)
+ in biggestTypeSize `div` 2 < amountOfCoreBndrs
+ && amountOfCoreBndrs > 4
+
+
+------------------------------------------------------------------------------
+-- | Pretty print a "deep dicts" warning.
+pprDeepDict :: [SrcSpan] -> Set CoreBndr -> SDoc
+pprDeepDict goodSpans vars =
+ let srcSpanList = if length goodSpans >= 3
+ then take 3 ((bullet <+>) . ppr <$> goodSpans) <> [text "..."]
+ else (bullet <+>) . ppr <$> goodSpans
+ in vcat [ text "Found a large chain of dictionaries produced in GHC Core."
+ , nest 2 $ text "A big instance chain that is generating a linear amount of core dictionaries."
+ $$ text "This is probably caused by instance induction on an unbalanced structure (like a type-level list)."
+ $$ text "Consider using a balanced structure (like a type-level tree)."
+ , blankLine
+ , text "Arising from:"
+ , nest 4 (vcat srcSpanList)
+ , blankLine
+ , text "Biggest dictionary: " <+> coloured colBlueFg (ppr $ biggestType vars)
+ , text "Size of type: " <+> coloured colBlueFg (int $ typeSizeWithoutKinds $ biggestType vars)
+ , text "Number of dictionaries: " <+> coloured colBlueFg (int $ Set.size vars)
+ , blankLine
+ ]
+
+
+------------------------------------------------------------------------------
+-- | Attempts to measure "how big" a type is. We count terminal type
+-- constructors, and type literals as 1. Kinds are right out. Chosen so that
+-- @'[1, 2, 3, 4]@ has size 4.
+typeSizeWithoutKinds :: Type -> Int
+typeSizeWithoutKinds LitTy {} = 1
+typeSizeWithoutKinds TyVarTy {} = 1
+typeSizeWithoutKinds (AppTy t1 t2) = typeSizeWithoutKinds t1 + typeSizeWithoutKinds t2
+typeSizeWithoutKinds (FunTy FUNTYARG t1 t2) = typeSizeWithoutKinds t1 + typeSizeWithoutKinds t2
+typeSizeWithoutKinds (ForAllTy (Bndr tv _) t) = typeSizeWithoutKinds (varType tv) + typeSizeWithoutKinds t
+typeSizeWithoutKinds (TyConApp tc []) =
+ let (kind_vars, _, _) = tcSplitNestedSigmaTys $ tyConKind tc
+ in 1 - length kind_vars
+typeSizeWithoutKinds (TyConApp tc ts) =
+ let (kind_vars, _, _) = tcSplitNestedSigmaTys $ tyConKind tc
+ in sum (fmap typeSizeWithoutKinds ts) - length kind_vars
+typeSizeWithoutKinds (CastTy ty _) = typeSizeWithoutKinds ty
+typeSizeWithoutKinds (CoercionTy _) = 0
+
diff --git a/test/BadTest.hs b/test/BadTest.hs
new file mode 100644
--- /dev/null
+++ b/test/BadTest.hs
@@ -0,0 +1,17 @@
+{-# OPTIONS_GHC -ddump-simpl -ddump-to-file #-}
+{-# OPTIONS_GHC -fplugin=CoreWarn #-}
+
+module BadTest where
+
+import Infra
+import Data.Proxy
+
+bad :: ()
+bad = requireEmptyClass @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 12])) $ Proxy
+
+really_bad :: ()
+really_bad = seq (requireEmptyClass @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])) Proxy)
+ (requireEmptyClass @(ToTree('[12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1])) Proxy)
+
+
+
diff --git a/test/GoodTest.hs b/test/GoodTest.hs
new file mode 100644
--- /dev/null
+++ b/test/GoodTest.hs
@@ -0,0 +1,12 @@
+{-# OPTIONS_GHC -ddump-simpl -ddump-to-file #-}
+{-# OPTIONS_GHC -fplugin=CoreWarn #-}
+
+module GoodTest where
+
+import Infra
+import Data.Proxy
+
+good :: ()
+good = requireEmptyClass $ Proxy @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10]))
+
+
diff --git a/test/InductionTest.hs b/test/InductionTest.hs
new file mode 100644
--- /dev/null
+++ b/test/InductionTest.hs
@@ -0,0 +1,24 @@
+{-# OPTIONS_GHC -ddump-simpl -ddump-to-file -dsuppress-uniques #-}
+{-# OPTIONS_GHC -fplugin=CoreWarn #-}
+
+module InductionTest where
+
+import Infra
+import Data.Proxy
+
+tree :: ()
+tree = requireEmptyClass $ Proxy @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 15, 16, 17, 18, 19, 20, 21, 22, 23, 24, 25, 26, 27, 28, 29, 30, 31, 32, 33, 34, 35, 36, 37, 38, 39, 40]))
+
+induction :: ()
+induction = requireInductionClass @('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12]) $ Proxy
+
+really_bad :: ()
+really_bad = seq (requireEmptyClass @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])) Proxy)
+ (requireEmptyClass @(ToTree('[12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1])) Proxy)
+
+really_really_bad :: ()
+really_really_bad = seq (requireEmptyClass @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])) Proxy)
+ (seq (requireEmptyClass @(ToTree('[12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1])) Proxy)
+ (seq (requireEmptyClass @(ToTree('[1, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12])) Proxy)
+ (requireEmptyClass @(ToTree('[12, 11, 10, 9, 8, 7, 6, 5, 4, 3, 2, 1])) Proxy)
+ ))
diff --git a/test/Infra.hs b/test/Infra.hs
new file mode 100644
--- /dev/null
+++ b/test/Infra.hs
@@ -0,0 +1,46 @@
+module Infra (requireEmptyClass, requireInductionClass, ToTree) where
+
+import Data.Kind (Type)
+import Data.Proxy
+
+data Tree a =
+ Zero
+ | One a
+ | Two a a
+ | Branch a (Tree a) (Tree a)
+
+class EmptyClass (xs :: Tree a) where
+
+class InductionClass (xs :: [a]) where
+
+instance InductionClass '[]
+instance InductionClass as => InductionClass (a ': as)
+
+requireInductionClass :: InductionClass xs => Proxy xs -> ()
+requireInductionClass _ = ()
+
+instance EmptyClass 'Zero
+instance EmptyClass ('One x)
+instance EmptyClass ('Two x1 x2)
+instance (EmptyClass l, EmptyClass r) => EmptyClass ('Branch x l r)
+
+-- Evens [0, 1, .. 9] == [0, 2, 4, 6, 8]
+type family Evens (xs :: [a]) :: [a] where
+ Evens '[] = '[]
+ Evens '[x] = '[x]
+ Evens (x ': _ ': xs) = x ': Evens xs
+
+-- Odds [0, 1, .. 9] == [1, 3, 5, 7, 9]
+type family Odds (xs :: [a]) :: [a] where
+ Odds '[] = '[]
+ Odds (_ ': xs) = Evens xs
+
+type family ToTree (xs :: [a]) :: Tree a where
+ ToTree '[] = 'Zero
+ ToTree '[x] = 'One x
+ ToTree '[x1, x2] = 'Two x1 x2
+ ToTree (x ': xs) = 'Branch x (ToTree (Evens xs)) (ToTree (Odds xs))
+
+requireEmptyClass :: EmptyClass xs => Proxy xs -> ()
+requireEmptyClass _ = ()
+
diff --git a/test/Main.hs b/test/Main.hs
new file mode 100644
--- /dev/null
+++ b/test/Main.hs
@@ -0,0 +1,5 @@
+module Main where
+
+main :: IO ()
+main = pure ()
+
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+module Spec where