core-warn (empty) → 0.1.0.0
raw patch · 14 files changed
+660/−0 lines, 14 filesdep +basedep +containersdep +containers-good-graphsetup-changed
Dependencies added: base, containers, containers-good-graph, core-warn, ghc, syb
Files
- CHANGELOG.md +5/−0
- LICENSE +30/−0
- README.md +86/−0
- Setup.hs +2/−0
- core-warn.cabal +57/−0
- src/CoreWarn.hs +220/−0
- src/Warn/Coercion.hs +50/−0
- src/Warn/Dictionary.hs +105/−0
- test/BadTest.hs +17/−0
- test/GoodTest.hs +12/−0
- test/InductionTest.hs +24/−0
- test/Infra.hs +46/−0
- test/Main.hs +5/−0
- test/Spec.hs +1/−0
+ CHANGELOG.md view
@@ -0,0 +1,5 @@+# Revision history for coercion-check++## 0.1.0.0 -- YYYY-mm-dd++* First version. Released on an unsuspecting world.
+ LICENSE view
@@ -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.
+ README.md view
@@ -0,0 +1,86 @@+<h1 align="center"> Core Warn </h1>+<p align="center">+ <a href="https://github.com/JonathanLorimer/core-warn/actions">+ <img src="https://img.shields.io/github/workflow/status/JonathanLorimer/core-warn/Haskell CI?style=flat-square" alt="CI badge"/>+ </a>+ <a href="https://haskell.org">+ <img src="https://img.shields.io/badge/Made%20in-Haskell-%235e5086?logo=haskell&style=flat-square" alt="made with Haskell"/>+ </a>+ <a href="https://hackage.haskell.org/package/core-warn">+ <img src="https://img.shields.io/hackage/v/core-warn.svg?logo=haskell&label=core-warn&style=flat-square" alt="hackage link" />+ </a>+</p>++## 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:<opt-name> #-}+```++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`
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ core-warn.cabal view
@@ -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 <https://github.com/JonathanLorimer/core-warn#readme>+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
+ src/CoreWarn.hs view
@@ -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+
+ src/Warn/Coercion.hs view
@@ -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++
+ src/Warn/Dictionary.hs view
@@ -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+
+ test/BadTest.hs view
@@ -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)+++
+ test/GoodTest.hs view
@@ -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]))++
+ test/InductionTest.hs view
@@ -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)+ ))
+ test/Infra.hs view
@@ -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 _ = ()+
+ test/Main.hs view
@@ -0,0 +1,5 @@+module Main where++main :: IO ()+main = pure ()+
+ test/Spec.hs view
@@ -0,0 +1,1 @@+module Spec where