packages feed

constraints-deriving (empty) → 1.0.0.0

raw patch · 34 files changed

+4110/−0 lines, 34 filesdep +basedep +bytestringdep +constraintsbuild-type:Customsetup-changed

Dependencies added: base, bytestring, constraints, constraints-deriving, filepath, ghc, ghc-paths, path, path-io

Files

+ LICENSE view
@@ -0,0 +1,30 @@+Copyright Artem Chirkin (c) 2019
+
+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 Artem Chirkin 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,83 @@+constraints-deriving
+==================================
+[![Build Status](https://secure.travis-ci.org/achirkin/constraints-deriving.svg)](http://travis-ci.org/achirkin/constraints-deriving)
+
+This project is based on the [constraints](http://hackage.haskell.org/package/constraints) library.
+Module `Data.Constraint.Deriving` provides a GHC Core compiler plugin that generates class instances.
+
+The main goal of this project is to make possible a sort of ad-hoc polymorphism that I wanted to
+implement in [easytensor](http://hackage.haskell.org/package/easytensor) for performance reasons:
+an umbrella type unifies multiple specialized type family backend instances;
+if the type instance is known, GHC picks a specialized (overlapping) class instance for a required function;
+otherwise, GHC resorts to a unified (overlappable) instance that is defined for the whole type family.
+
+To use the plugin, add
+```Haskell
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+```
+to the header of your module.
+For debugging, add a plugin option `dump-instances`:
+```Haskell
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+```
+to the header of your file; it will print all instances declared in the module (hand-written and auto-generated).
+To enable much more verbose debug output, use library flag `dev` (for debugging the plugin itself).
+
+Check out `example` folder for a motivating use case (enabled with flag `examples`).
+
+The plugin is controlled via GHC annotations; there are two types of annotations corresponding to two plugin passes.
+Both passes are core-to-core, which means the plugin runs after typechecker,
+which in turn means **the generated class instances are available only outside of the module**.
+A sort of inconvenience you may have experienced with template haskell 😉.
+
+### DeriveAll
+
+`DeriveAll` plugin pass inspects a newtype declaration.
+To enable `DeriveAll` for a newtype `Foo`, add an annotation as follows:
+```Haskell
+{-# ANN type Foo DeriveAll #-}
+newtype Foo a = ...
+```
+check out [`test/Spec/`](https://github.com/achirkin/constraints-deriving/tree/master/test/Spec) for [more examples](https://github.com/achirkin/constraints-deriving/blob/master/test/Spec/DeriveAll04.hs#L19-L20).
+
+`DeriveAll` plugin pass looks through all possible type instances (in the presence of type families) of the base type,
+and copies all class instances for the newtype wrapper.
+
+Sometimes, you may need to refine the relation between the base type and the newtype;
+you can do this via a special `type family DeriveContext newtype :: Constraint`.
+By adding equality constraints, you can specify custom dependencies between type variables present in the newtype declaration
+(e.g. [`test/Spec/DeriveAll01.hs`](https://github.com/achirkin/constraints-deriving/blob/master/test/Spec/DeriveAll01.hs#L24)).
+By adding class constraints, you force these class constraints for all generated class instances
+(e.g. in [`test/Spec/DeriveAll02.hs`](https://github.com/achirkin/constraints-deriving/blob/master/test/Spec/DeriveAll02.hs#L37)
+ all class instances of `BazTy a b c d e f` have an additional constraint `Show e`).
+
+
+Note, the internal machinery is different from `GeneralizedNewtypeDeriving` approach:
+rather than coercing every function in the instance definition from the base type to the newtype,
+it coerces the whole instance dictionary.
+
+
+### ToInstance
+
+`ToInstance` plugin pass converts a top-level `Ctx => Dict (Class t1..tn)` value declaration into
+an instance of the form `instance Ctx => Class t1..tn`.
+Thus, one can write arbitrary Haskell code (returning a class dictionary) to be executed every time
+an instance is looked up by the GHC machinery.
+To derive an instance this way, use  `ToInstance (x :: OverlapMode)` for a declaration, e.g. as follows:
+```Haskell
+newtype Foo t = Foo t
+
+{-# ANN deriveEq (ToInstance NoOverlap) #-}
+deriveEq :: Eq t => Dict (Eq (Foo t))
+deriveEq = mapDict (unsafeDerive Foo) Dict
+
+-- the result of the above is equal to
+-- deriving instance Eq t => Eq (Foo t)
+```
+You can find a more meaningful example in [`test/Spec/ToInstance01.hs`](https://github.com/achirkin/constraints-deriving/blob/master/test/Spec/ToInstance01.hs#L45-L47) or
+[`example/Lib/VecBackend.hs`](https://github.com/achirkin/constraints-deriving/blob/master/example/Lib/VecBackend.hs).
+
+## Further work
+
+One thing the `DeriveAll` pass misses is an option to blacklist some classes to avoid generating undesired instances.
+Furthermore, its derivation mechanics currently may break functional dependencies (untested).
+ Setup.hs view
@@ -0,0 +1,81 @@+{-
+Here is a very unfortunate hack that allows me to re-export modules of
+the "constraints" library if flag "constraints" is enabled.
+
+I have to do this because:
+
+ * if flag "constraints" is disabled, the library exports its own modules
+   (copied from the "constraints" library, thus the same API);
+
+ * if I add reexported-modules in the package description, cabal check
+   complains for duplicate modules
+   (even though they are under mutually exclusive conditions);
+
+ * I still want library users import the modules without PackageImports or alike
+   independently of their choice of flags.
+ -}
+{-# OPTIONS_GHC -Wall #-}
+{-# LANGUAGE CPP #-}
+
+#ifndef MIN_VERSION_Cabal
+#define MIN_VERSION_Cabal(x,y,z) 0
+#endif
+
+module Main (main) where
+
+import Distribution.PackageDescription
+import Distribution.Simple
+import qualified Distribution.ModuleName as ModuleName
+#if MIN_VERSION_Cabal(2,0,0)
+import Distribution.Types.CondTree (CondBranch(CondBranch))
+#endif
+
+main :: IO ()
+main = defaultMainWithHooks simpleUserHooks
+  { confHook = \(gpd, hbi) -> confHook simpleUserHooks (addReexportsGPD gpd, hbi) }
+
+addReexportsGPD :: GenericPackageDescription -> GenericPackageDescription
+addReexportsGPD gpd = gpd { condLibrary = addReexportsCT <$> condLibrary gpd }
+
+
+addReexportsCT :: CondTree ConfVar [Dependency] Library
+               -> CondTree ConfVar [Dependency] Library
+addReexportsCT ct = ct
+    { condTreeComponents = reexportBranch : condTreeComponents ct }
+  where
+    constraintsCondition = Var (Flag (mkFlagName "constraints"))
+    reexportContent   = mempty
+      { reexportedModules =
+         [ ModuleReexport
+             { moduleReexportOriginalPackage = Just (mkPackageName "constraints")
+             , moduleReexportOriginalName = ModuleName.fromString "Data.Constraint"
+             , moduleReexportName = ModuleName.fromString "Data.Constraint"
+             }
+         , ModuleReexport
+             { moduleReexportOriginalPackage = Just (mkPackageName "constraints")
+             , moduleReexportOriginalName = ModuleName.fromString "Data.Constraint.Unsafe"
+             , moduleReexportName = ModuleName.fromString "Data.Constraint.Unsafe"
+             }
+         ]
+      }
+    constraintsTrueTree = CondNode
+      { condTreeData        = reexportContent
+      , condTreeConstraints = []
+      , condTreeComponents  = []
+      }
+    constraintsFalseTree = Nothing
+    reexportBranch =
+#if MIN_VERSION_Cabal(2,0,0)
+      CondBranch
+#else
+      (,,)
+#endif
+        constraintsCondition constraintsTrueTree constraintsFalseTree
+
+#if !MIN_VERSION_Cabal(2,0,0)
+mkFlagName :: String -> FlagName
+mkFlagName = FlagName
+
+mkPackageName :: String -> PackageName
+mkPackageName = PackageName
+#endif
+ constraints-deriving.cabal view
@@ -0,0 +1,127 @@+cabal-version: 1.24
++-- This file has been generated from package.yaml by hpack version 0.31.1.+--+-- see: https://github.com/sol/hpack+--+-- hash: 17a01f667d137f6141a5e8187c79745cfa14e212066be7fee4ddd4c39dd1ddc8++name:           constraints-deriving+version:        1.0.0.0+synopsis:       Manipulating constraints and deriving class instances programmatically.+description:    The library provides a plugin to derive class instances programmatically. Please see the README on GitHub at <https://github.com/achirkin/constraints-deriving#readme>+category:       Constraints+homepage:       https://github.com/achirkin/constraints-deriving#readme+bug-reports:    https://github.com/achirkin/constraints-deriving/issues+author:         Artem Chirkin+maintainer:     achirkin@users.noreply.github.com+copyright:      Copyright: (c) 2019 Artem Chirkin+license:        BSD3+license-file:   LICENSE+build-type:     Custom+extra-source-files:+    README.md+    test/Spec/DeriveAll01.hs+    test/Spec/DeriveAll02.hs+    test/Spec/DeriveAll03.hs+    test/Spec/DeriveAll04.hs+    test/Spec/DeriveAll05.hs+    test/Spec/ToInstance01.hs+    test/out/DeriveAll01.stderr+    test/out/DeriveAll02.stderr+    test/out/DeriveAll03.stderr+    test/out/DeriveAll04.stderr+    test/out/DeriveAll05.stderr+    test/out/ToInstance01.stderr+    test/out/DeriveAll01.stdout+    test/out/DeriveAll02.stdout+    test/out/DeriveAll03.stdout+    test/out/DeriveAll04.stdout+    test/out/DeriveAll05.stdout+    test/out/ToInstance01.stdout++source-repository head+  type: git+  location: https://github.com/achirkin/constraints-deriving++custom-setup+  setup-depends:+      Cabal+    , base++flag constraints+  description: Use vanilla constraints package as a dependency instead of the manual minimalistic definitions copied from there.+  manual: True+  default: False++flag debug+  description: Show debug trace info (used only for library develpoment)+  manual: True+  default: False++flag examples+  description: Whether to build examples+  manual: True+  default: False++library+  exposed-modules:+      Data.Constraint.Bare+      Data.Constraint.Deriving+      Data.Constraint.Deriving.DeriveAll+      Data.Constraint.Deriving.ToInstance+  other-modules:+      Data.Constraint.Deriving.CorePluginM+  hs-source-dirs:+      src+  ghc-options: -Wall+  build-depends:+      base >=4.9 && <5+    , ghc >=8.0.1+  if flag(debug)+    cpp-options: -DPLUGIN_DEBUG+  if flag(constraints)+    build-depends:+        constraints >=0.6+  else+    exposed-modules:+        Data.Constraint+        Data.Constraint.Unsafe+    hs-source-dirs:+        src-constraints+  default-language: Haskell2010++executable deriving-example+  main-is: Main.hs+  other-modules:+      Lib.BackendFamily+      Lib.VecBackend+      Lib.Vector+  hs-source-dirs:+      example+  ghc-options: -Wall+  build-depends:+      base >=4.9 && <5+    , constraints-deriving+  if flag(examples)+    ghc-options: -dcore-lint+  else+    buildable: False+  default-language: Haskell2010++test-suite functional-tests+  type: exitcode-stdio-1.0+  main-is: Spec.hs+  hs-source-dirs:+      test+  ghc-options: -Wall+  build-depends:+      base >=4.9 && <5+    , bytestring+    , constraints-deriving+    , filepath+    , ghc+    , ghc-paths+    , path+    , path-io+  default-language: Haskell2010
+ example/Lib/BackendFamily.hs view
@@ -0,0 +1,224 @@+{-# LANGUAGE CPP                    #-}
+{-# LANGUAGE ConstraintKinds        #-}
+{-# LANGUAGE DataKinds              #-}
+{-# LANGUAGE DefaultSignatures      #-}
+{-# LANGUAGE ExplicitNamespaces     #-}
+{-# LANGUAGE FlexibleContexts       #-}
+{-# LANGUAGE FlexibleInstances      #-}
+{-# LANGUAGE GADTs                  #-}
+{-# LANGUAGE MagicHash              #-}
+{-# LANGUAGE MultiParamTypeClasses  #-}
+{-# LANGUAGE PolyKinds              #-}
+{-# LANGUAGE RankNTypes             #-}
+{-# LANGUAGE ScopedTypeVariables    #-}
+{-# LANGUAGE StandaloneDeriving     #-}
+{-# LANGUAGE TypeApplications       #-}
+{-# LANGUAGE TypeFamilies           #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# LANGUAGE TypeOperators          #-}
+{-# LANGUAGE UndecidableInstances   #-}
+
+{- |
+  This module contains actual implementation of the `Backend` type family.
+
+  The idea is that this module does not expose any implementation details;
+  one can even implement multiple copies of this file depending on the compiler or package flags,
+  (such as the presence of SIMD extensions).
+  
+  In this example, I provide four implementations, depending on the dimensionality of the vector.
+  Note, that no evidence of the implementation details is exported.
+ -}
+module Lib.BackendFamily
+  ( Backend, DataElemType, DataDims
+  , KnownBackend ()
+  , inferBackendInstance
+    -- constructing data
+  , bCons, bUncons, bNil
+  ) where
+
+
+import Data.Constraint
+import Debug.Trace
+import GHC.Base
+import GHC.TypeLits    (type (+), type (-), CmpNat, KnownNat, Nat, natVal)
+#if __GLASGOW_HASKELL__ < 804
+import Data.Semigroup
+#endif
+
+
+-- backend type level definitions
+data UnitBase (t :: Type) = UnitBase
+  deriving (Eq, Ord, Show)
+
+newtype ScalarBase (t :: Type) = ScalarBase { _unScalarBase :: t }
+  deriving (Eq, Ord, Show)
+
+data Vec2Base (t :: Type) = Vec2Base t t
+  deriving (Eq, Ord, Show)
+
+newtype ListBase (t :: Type) (n :: Nat) = ListBase { _unListBase :: [t] }
+  deriving (Eq, Ord, Show)
+
+-- backend mappings
+type family Backend (t :: Type) (n :: Nat) = (v :: Type) | v -> t n where
+    Backend t  0 = UnitBase t
+    Backend t  1 = ScalarBase t
+    Backend t  2 = Vec2Base t
+    Backend t  n = ListBase t n
+
+-- ideally, bijection in the backend mapping allows to identify t and n,
+-- but compiler does not like it.
+
+type family DataElemType (backend :: Type) :: Type
+type instance DataElemType (UnitBase t)   = t
+type instance DataElemType (ScalarBase t) = t
+type instance DataElemType (Vec2Base t)   = t
+type instance DataElemType (ListBase t _) = t
+
+type family DataDims (backend :: Type) :: Nat
+type instance DataDims (UnitBase _)   = 0
+type instance DataDims (ScalarBase _) = 1
+type instance DataDims (Vec2Base _)   = 2
+type instance DataDims (ListBase _ n) = n
+
+-- backend term level definition (GADT)
+data BackendSing (backend :: Type) where
+  BS0 :: (Backend t 0 ~ UnitBase t  , n ~ 0) => BackendSing (UnitBase t)
+  BS1 :: (Backend t 1 ~ ScalarBase t, n ~ 1) => BackendSing (ScalarBase t)
+  BS2 :: (Backend t 2 ~ Vec2Base t  , n ~ 2) => BackendSing (Vec2Base t)
+  BSn :: (Backend t n ~ ListBase t n, CmpNat n 2 ~ 'GT) => BackendSing (ListBase t n)
+
+
+deriving instance Eq (BackendSing backend)
+deriving instance Ord (BackendSing backend)
+deriving instance Show (BackendSing backend)
+
+
+-- | A framework for using Array type family instances.
+class KnownBackend (t :: Type) where
+    -- | Get Array type family instance
+    bSing :: BackendSing t
+    default bSing :: ( Coercible (Backend (DataElemType t) (DataDims t)) t
+                     , KnownBackend (Backend (DataElemType t) (DataDims t))
+                     )
+                  => BackendSing t
+    bSing = unsafeCoerce# (bSing @(Backend (DataElemType t) (DataDims t)))
+
+
+
+instance Semigroup (UnitBase t) where
+  UnitBase <> UnitBase = UnitBase
+
+instance Monoid (UnitBase t) where
+  mempty = UnitBase
+  mappend = (<>)
+
+
+instance Num t => Semigroup (ScalarBase t) where
+  ScalarBase a <> ScalarBase b = ScalarBase (a + b)
+
+instance Num t => Monoid (ScalarBase t) where
+  mempty = ScalarBase 0
+  mappend = (<>)
+
+instance Num t => Semigroup (Vec2Base t) where
+  Vec2Base a1 a2 <> Vec2Base b1 b2 = Vec2Base (a1 + b1) (a2 + b2)
+
+instance Num t => Monoid (Vec2Base t) where
+  mempty = Vec2Base 0 0
+  mappend = (<>)
+
+instance Num t => Semigroup (ListBase t n) where
+  ListBase as <> ListBase bs = ListBase $ zipWith (+) as bs
+
+instance (Num t, KnownNat n) => Monoid (ListBase t n) where
+  mempty = r
+    where
+      r = ListBase $ replicate (fromInteger $ natVal r) 0
+  mappend = (<>)
+
+instance KnownBackend (UnitBase t) where
+    bSing = BS0
+instance KnownBackend (ScalarBase t) where
+    bSing = BS1
+instance KnownBackend (Vec2Base t) where
+    bSing = BS2
+instance CmpNat n 2 ~ 'GT => KnownBackend (ListBase t n) where
+    bSing = case ( unsafeCoerce#
+                     (Dict :: Dict (ListBase t n ~ ListBase t n) )
+                           :: Dict (ListBase t n ~ Backend  t n)
+                 ) of
+      Dict -> BSn
+
+
+-- This function determines the logic of instance selection
+-- for the type  b
+inferBackendInstance
+  :: forall b c
+   . ( KnownBackend b
+     , c (UnitBase (DataElemType b))
+     , c (ScalarBase (DataElemType b))
+     , c (Vec2Base (DataElemType b))
+     , c (ListBase (DataElemType b) (DataDims b))
+     )
+  => Dict (c b)
+inferBackendInstance = case (bSing :: BackendSing b) of
+    BS0 -> trace "---------- Selecting UnitBase" Dict
+    BS1 -> trace "---------- Selecting ScalarBase" Dict
+    BS2 -> trace "---------- Selecting Vec2Base" Dict
+    BSn -> trace "---------- Selecting ListBase" Dict
+{-# INLINE inferBackendInstance #-}
+
+
+bUncons :: forall t n m
+         . KnownBackend (Backend t n)
+        => Backend t n
+        -> Either ( Dict ( n ~ 0
+                         , n ~ DataDims (Backend t n)
+                         , t ~ DataElemType (Backend t n)
+                         ))
+                  ( Dict ( KnownBackend (Backend t m)
+                         , n ~ (m + 1)
+                         , m ~ (n - 1)
+                         , n ~ DataDims (Backend t n)
+                         , m ~ DataDims (Backend t m)
+                         , t ~ DataElemType (Backend t n)
+                         , t ~ DataElemType (Backend t m)
+                         )
+                  , t, Backend t m )
+bUncons x = case dataTypeDims x of
+  Dict -> case bSing @(Backend t n) of
+    BS0 -> Left Dict
+    BS1 -> case unsafeDict @(n ~ n, m ~ m) @(n ~ 1, m ~ 0) Dict of
+      Dict -> case x of ScalarBase a -> Right (Dict, a, UnitBase)
+    BS2 -> case unsafeDict @(n ~ n, m ~ m) @(n ~ 2, m ~ 1) Dict of
+      Dict -> case x of Vec2Base a b -> Right (Dict, a, ScalarBase b)
+    BSn -> case x of
+      ListBase [a,b,c] -> case unsafeDict @(n ~ n, m ~ m) @(n ~ 3, m ~ 2) Dict of
+        Dict -> Right (Dict, a, Vec2Base b c)
+      ListBase (a:as) -> case unsafeDict
+                                @(n ~ n, m ~ m, CmpNat 3 2 ~ 'GT, Backend t m ~ Backend t m)
+                                @(n ~ (m + 1), m ~ (n - 1), CmpNat m 2 ~ 'GT, Backend t m ~ ListBase t m)
+                                Dict of
+        Dict -> Right (Dict, a, ListBase @t @m as)
+      ListBase _      -> error "Unexpected-length vector"
+
+unsafeDict :: forall a b . a => Dict a -> Dict b
+unsafeDict _ = unsafeCoerce# (Dict @a)
+
+dataTypeDims :: forall t n . Backend t n -> Dict (t ~ DataElemType (Backend t n), n ~ DataDims (Backend t n))
+dataTypeDims _ = unsafeCoerce# (Dict @(t ~ t, n ~ n))
+
+--  Hmm, would be interesting to "provide" KnownBackend (Backend t (n+1))
+bCons :: forall t n
+       . KnownBackend (Backend t n)
+      => t -> Backend t n -> Backend t (n + 1)
+bCons a as = case dataTypeDims @t @n as of
+  Dict -> case bSing @(Backend t n) of
+    BS0 -> ScalarBase a
+    BS1 -> case as of ScalarBase b -> Vec2Base a b
+    BS2 -> case as of Vec2Base b c -> ListBase [a,b,c]
+    BSn -> case as of ListBase as' -> unsafeCoerce# (ListBase (a : as'))
+
+bNil :: Backend t 0
+bNil = UnitBase
+ example/Lib/VecBackend.hs view
@@ -0,0 +1,109 @@+{-# LANGUAGE CPP                  #-}
+{-# LANGUAGE ConstraintKinds      #-}
+{-# LANGUAGE DataKinds            #-}
+{-# LANGUAGE FlexibleContexts     #-}
+{-# LANGUAGE FlexibleInstances    #-}
+{-# LANGUAGE GADTs                #-}
+{-# LANGUAGE PatternSynonyms      #-}
+{-# LANGUAGE RankNTypes           #-}
+{-# LANGUAGE RoleAnnotations      #-}
+{-# LANGUAGE ScopedTypeVariables  #-}
+{-# LANGUAGE TypeApplications     #-}
+{-# LANGUAGE TypeFamilies         #-}
+{-# LANGUAGE TypeOperators        #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+{- |
+  This is where the magic happens.
+
+  Via combination of DeriveAll and ToInstance plugin passes
+  I create a system of overlapping type class instances for `VecBackend` type.
+  This way, if GHC knows which backend (type instance of `Backend`) is behind `VecBackend`,
+  it can select overlapping class instance for it;
+  overwise, it selects overlappable instance based on `KnownBackend` constraint.
+  -}
+module Lib.VecBackend where
+
+
+import Data.Constraint
+import Data.Constraint.Deriving
+import Data.Constraint.Unsafe
+import GHC.Base
+import GHC.TypeLits             (KnownNat, Nat)
+import Unsafe.Coerce
+#if __GLASGOW_HASKELL__ < 804
+import Data.Semigroup
+#endif
+
+import Lib.BackendFamily
+
+-- Try to comment out the annotation;
+-- You will see that the compiler has to select type class instances at runtime more often.
+{-# ANN type VecBackend DeriveAll #-}
+type role VecBackend phantom phantom representational
+-- I need two layers of wrappers to provide default overlappable instances to
+-- all type classes using KnownBackend mechanics.
+-- Type arguments are redundant here;
+-- nevertheless, they improve readability of error messages.
+newtype VecBackend (t :: Type) (n :: Nat) (backend :: Type)
+  = VecBackend { _getBackend :: backend }
+type instance DataElemType (VecBackend t _ _) = t
+type instance DataDims (VecBackend _  n _) = n
+-- I use this type instance to inform `DeriveAll` core plugin that backend is an instance
+-- of type family `Backend t n`.
+-- This allows the plugin to find all possible instances of the type family and
+-- then lookup corresponding class instances.
+-- Otherwise, the plugin would have to derive all instances for all types in scope,
+-- because the newtype declaration is too general without these additional constraints.
+type instance DeriveContext (VecBackend t n b) = b ~ Backend t n
+
+
+
+{-# ANN inferEq (ToInstance Overlappable) #-}
+inferEq :: forall t n b . ( KnownBackend b, Eq t) => Dict (Eq (VecBackend t n b))
+inferEq = mapDict toVecBackend
+        . mapDict (Sub inferBackendInstance)
+        $ inferBase @t @n @b undefined
+
+{-# ANN inferShow (ToInstance Overlappable) #-}
+inferShow :: forall t n b . ( KnownBackend b, Show t)
+          => Dict (Show (VecBackend t n b))
+inferShow = mapDict toVecBackend
+          . mapDict (Sub inferBackendInstance)
+          $ inferBase @t @n @b undefined
+
+{-# ANN inferOrd (ToInstance Overlappable) #-}
+inferOrd :: forall t n b . ( KnownBackend b, Ord t)
+         => Dict (Ord (VecBackend t n b))
+inferOrd = mapDict toVecBackend
+         . mapDict (Sub inferBackendInstance)
+         $ inferBase @t @n @b undefined
+
+{-# ANN inferSemigroup (ToInstance Overlappable) #-}
+inferSemigroup :: forall t n b . ( KnownBackend b, Num t)
+               => Dict (Semigroup (VecBackend t n b))
+inferSemigroup = mapDict toVecBackend
+               . mapDict (Sub inferBackendInstance)
+               $ inferBase @t @n @b undefined
+
+{-# ANN inferMonoid (ToInstance Overlappable) #-}
+inferMonoid :: forall t n b . ( KnownBackend b, Num t, KnownNat n)
+            => Dict (Monoid (VecBackend t n b))
+inferMonoid = mapDict toVecBackend
+            . mapDict (Sub inferBackendInstance)
+            $ inferBase @t @n @b undefined
+
+-- This is the rule that cannot be encoded in the type system, but enforced
+-- as an invariant: VecBackend t n b implies DeriveContext t n b
+inferBase :: VecBackend t n b
+          -> Dict (b ~ Backend t n, t ~ DataElemType b, n ~ DataDims b)
+inferBase _ = unsafeCoerce
+  (Dict :: Dict (b ~ b, t ~ t, n ~ n) )
+{-# INLINE inferBase #-}
+
+-- VecBackend is the newtype wrapper over b.
+-- It has the same represenation and I expect it to have the same instance behavior.
+toVecBackend :: forall c t n b . c b :- c (VecBackend t n b)
+toVecBackend = unsafeDerive VecBackend
+{-# INLINE toVecBackend #-}
+ example/Lib/Vector.hs view
@@ -0,0 +1,117 @@+{-# LANGUAGE CPP                        #-}
+{-# LANGUAGE DataKinds                  #-}
+{-# LANGUAGE ExplicitNamespaces         #-}
+{-# LANGUAGE FlexibleContexts           #-}
+{-# LANGUAGE FlexibleInstances          #-}
+{-# LANGUAGE GADTs                      #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE MagicHash                  #-}
+{-# LANGUAGE MultiParamTypeClasses      #-}
+{-# LANGUAGE PatternSynonyms            #-}
+{-# LANGUAGE RoleAnnotations            #-}
+{-# LANGUAGE ScopedTypeVariables        #-}
+{-# LANGUAGE StandaloneDeriving         #-}
+{-# LANGUAGE TypeApplications           #-}
+{-# LANGUAGE TypeFamilies               #-}
+{-# LANGUAGE TypeOperators              #-}
+{-# LANGUAGE UndecidableInstances       #-}
+{-# LANGUAGE ViewPatterns               #-}
+{- |
+  This is an example of using constraints-deriving plugin for optimization.
+
+  This module presents a "front-end"  Vector data type visible to a user.
+  It is a simple newtype wrapper over a "backend" data type family.
+  Behind the scenes, the compiler chooses the most efficient representations
+  for the backend based on a type family `Backend t n`.
+  For example, if the compiler knows that the size of a vector is 1,
+  than the `Vector t 1` type is a newtype wrapper over `t`,
+  and GHC statically uses all type class instances for `t`, sidestepping dynamic instance elaboration.
+  But, if GHC does not know the dimensionality of the vector statically,
+  it selects class instances dynamically at runtime.  
+ -}
+module Lib.Vector
+  ( -- * Data types
+    Vector (Z, (:*))
+  , SomeVector (..), KnownBackend (), Backend
+  , Nat
+  ) where
+
+
+#if __GLASGOW_HASKELL__ < 804
+import Data.Semigroup
+#endif
+import Data.Constraint
+import GHC.Base        (Type, unsafeCoerce#)
+import GHC.TypeLits    (type (+), type (-), KnownNat, Nat)
+
+import Lib.BackendFamily
+import Lib.VecBackend
+
+
+newtype Vector (t :: Type) (n ::Nat) = Vector (VecBackend t n (Backend t n))
+
+pattern Z :: forall t n
+           . KnownBackend (Vector t n)
+          => n ~ 0
+          => Vector t n
+pattern Z <- (vUncons -> Left Dict)
+  where
+    Z = Vector (VecBackend bNil)
+
+pattern (:*) :: forall t n
+              . KnownBackend (Vector t n)
+             => forall m
+              . (KnownBackend (Vector t m), n ~ (m + 1), m ~ (n - 1))
+             => t -> Vector t m -> Vector t n
+pattern (:*) x xs <- (vUncons -> Right (Dict, x, xs))
+  where
+    (:*) = vCons
+infixr 7 :*
+#if __GLASGOW_HASKELL__ >= 802
+{-# Complete Z, (:*) #-}
+#endif
+
+vUncons :: forall t n m
+         . KnownBackend (Vector t n)
+        => Vector t n
+        -> Either ( Dict ( n ~ 0
+                         , n ~ DataDims (Vector t n)
+                         , t ~ DataElemType (Vector t n)
+                         ))
+                  ( Dict ( KnownBackend (Vector t m)
+                         , n ~ (m + 1)
+                         , m ~ (n - 1)
+                         , n ~ DataDims (Vector t n)
+                         , m ~ DataDims (Vector t m)
+                         , t ~ DataElemType (Vector t n)
+                         , t ~ DataElemType (Vector t m)
+                         )
+                  , t, Vector t m )
+vUncons = case underiveKB @t @n of Dict -> unsafeCoerce# (bUncons @t @n @m)
+
+vCons :: forall t n
+       . KnownBackend (Vector t n)
+      => t -> Vector t n -> Vector t (n + 1)
+vCons = case underiveKB @t @n of Dict -> unsafeCoerce# (bCons @t @n)
+
+
+data SomeVector (t :: Type) where
+  SomeVector :: (KnownNat (n :: Nat), KnownBackend (Backend t n))
+             => Vector t n -> SomeVector t
+
+
+type instance DataElemType (Vector t n) = t
+type instance DataDims (Vector t n) = n
+
+instance (KnownBackend (Vector t n), Show t) => Show (Vector t n) where
+  show Z         = "Z"
+  show (x :* xs) = show x ++ " :* " ++ show xs
+
+instance KnownBackend (Backend t n) => KnownBackend (Vector t n)
+deriving instance Eq (VecBackend t n (Backend t n)) => Eq (Vector t n)
+deriving instance Ord (VecBackend t n (Backend t n)) => Ord (Vector t n)
+deriving instance Semigroup (VecBackend t n (Backend t n)) => Semigroup (Vector t n)
+deriving instance Monoid (VecBackend t n (Backend t n)) => Monoid (Vector t n)
+
+underiveKB :: forall t n . KnownBackend (Vector t n) => Dict (KnownBackend (Backend t n))
+underiveKB = unsafeCoerce# (Dict @(KnownBackend (Vector t n)))
+ example/Main.hs view
@@ -0,0 +1,35 @@+{-# LANGUAGE CPP       #-}
+{-# LANGUAGE DataKinds #-}
+module Main (main) where
+
+#if __GLASGOW_HASKELL__ < 804
+import           Data.Semigroup
+#endif
+import           Lib.Vector
+
+
+main :: IO ()
+main = do
+    print $ Z <> (mempty :: Vector Double 0)
+    print $ (7 :: Double) :* Z <> 15 :* Z
+    print $ (7 :: Double) :* Z <> mempty 
+    print $ mempty <> 2 :* 6 :* Z <> v2
+    () <- case v2 of
+      a :* as -> print $ a :* Z <> as
+    print $ mempty <> 9 :* 8 :* 7 :* 6 :* 5 :* Z
+                   <> 1 :* 2 :* 3 :* 4 :* 5 :* (Z :: Vector Double 0)
+    case sdf2 of
+      SomeVector x -> print $ mappend x x <> mempty
+    case sdf7 of
+      SomeVector x -> print $ x <> x <> x <> mempty <> x
+  where
+    -- The backend for v2 is known statically;
+    -- GHC will pick up all instances for Vec2Base
+    v2 = 3 :* 12 :* Z :: Vector Double 2
+    -- The two vectors below hide their dimensionality until runtime.
+    -- The only thing GHC knows is that they have instances of KnownBackend;
+    -- thus, it will lookup the rest of required type class instances via KnownBackend route.
+    sdf2 = SomeVector $ (2::Int) :* 6 :* Z
+    sdf7 = SomeVector $ (1::Float)
+      :* 2 :* 3 :* 4 :* 5 :* 16 :* 92 :* Z
+
+ src-constraints/Data/Constraint.hs view
@@ -0,0 +1,786 @@+{-
+Copyright 2011-2015 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.
+ -}
+{-# LANGUAGE FunctionalDependencies #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE EmptyDataDecls #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UnicodeSyntax #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Constraint
+-- Copyright   :  (C) 2011-2015 Edward Kmett,
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is taken from
+-- <https://github.com/ekmett/constraints/blob/963c0e904ad48a5cec29a0cb649622d8c1872af4/src/Data/Constraint.hs  constraints:Data.Constraint>
+-- A few things have been cut from the module to remove dependencies.
+-- 
+--
+----------------------------------------------------------------------------
+module Data.Constraint
+  (
+  -- * The Kind of Constraints
+    Constraint
+  -- * Dictionary
+  , Dict(Dict)
+  , HasDict(..)
+  , withDict
+  , (\\)
+  -- * Entailment
+  , (:-)(Sub)
+  , type (⊢)
+  , weaken1, weaken2, contract
+  , strengthen1, strengthen2
+  , (&&&), (***)
+  , trans, refl
+  , Bottom(no)
+  , top, bottom
+  -- * Dict is fully faithful
+  , mapDict
+  , unmapDict
+  -- * Reflection
+  , Class(..)
+  , (:=>)(..)
+  ) where
+import Control.Applicative
+import Control.Category
+import Control.Monad
+import Data.Complex
+#if __GLASGOW_HASKELL__ >= 800 && __GLASGOW_HASKELL__ < 806
+import Data.Kind
+#endif
+import Data.Ratio
+#if !MIN_VERSION_base(4,11,0)
+import Data.Semigroup
+#endif
+import Data.Data hiding (TypeRep)
+import qualified GHC.Exts as Exts (Any)
+import GHC.Exts (Constraint)
+import Data.Bits (Bits)
+import Data.Functor.Identity (Identity)
+import Numeric.Natural (Natural)
+import Data.Word (Word)
+import Data.Coerce (Coercible)
+import Data.Type.Coercion(Coercion(..))
+#if MIN_VERSION_base(4,10,0)
+import Data.Type.Equality ((:~~:)(..), type (~~))
+import Type.Reflection (TypeRep, typeRepKind, withTypeable)
+#endif
+
+-- | Values of type @'Dict' p@ capture a dictionary for a constraint of type @p@.
+--
+-- e.g.
+--
+-- @
+-- 'Dict' :: 'Dict' ('Eq' 'Int')
+-- @
+--
+-- captures a dictionary that proves we have an:
+--
+-- @
+-- instance 'Eq' 'Int
+-- @
+--
+-- Pattern matching on the 'Dict' constructor will bring this instance into scope.
+--
+data Dict :: Constraint -> * where
+  Dict :: a => Dict a
+  deriving Typeable
+
+
+instance (Typeable p, p) => Data (Dict p) where
+  gfoldl _ z Dict = z Dict
+  toConstr _ = dictConstr
+  gunfold _ z c = case constrIndex c of
+    1 -> z Dict
+    _ -> error "gunfold"
+  dataTypeOf _ = dictDataType
+
+dictConstr :: Constr
+dictConstr = mkConstr dictDataType "Dict" [] Prefix
+
+dictDataType :: DataType
+dictDataType = mkDataType "Data.Constraint.Dict" [dictConstr]
+
+deriving instance Eq (Dict a)
+deriving instance Ord (Dict a)
+deriving instance Show (Dict a)
+
+-- | Witnesses that a value of type @e@ contains evidence of the constraint @c@.
+--
+-- Mainly intended to allow ('\\') to be overloaded, since it's a useful operator.
+class HasDict c e | e -> c where
+  evidence :: e -> Dict c
+
+instance HasDict a (Dict a) where
+  evidence = Prelude.id
+
+instance a => HasDict b (a :- b) where
+  evidence (Sub x) = x
+
+instance HasDict (Coercible a b) (Coercion a b) where
+  evidence Coercion = Dict
+
+instance HasDict (a ~ b) (a :~: b) where
+  evidence Refl = Dict
+
+#if MIN_VERSION_base(4,10,0)
+instance HasDict (a ~~ b) (a :~~: b) where
+  evidence HRefl = Dict
+
+instance HasDict (Typeable k, Typeable a) (TypeRep (a :: k)) where
+  evidence tr = withTypeable tr $ withTypeable (typeRepKind tr) Dict
+#endif
+
+-- | From a 'Dict', takes a value in an environment where the instance
+-- witnessed by the 'Dict' is in scope, and evaluates it.
+--
+-- Essentially a deconstruction of a 'Dict' into its continuation-style
+-- form.
+--
+-- Can also be used to deconstruct an entailment, @a ':-' b@, using a context @a@.
+--
+-- @
+-- withDict :: 'Dict' c -> (c => r) -> r
+-- withDict :: a => (a ':-' c) -> (c => r) -> r
+-- @
+withDict :: HasDict c e => e -> (c => r) -> r
+withDict d r = case evidence d of
+                 Dict -> r
+
+infixl 1 \\ -- required comment
+
+-- | Operator version of 'withDict', with the arguments flipped
+(\\) :: HasDict c e => (c => r) -> e -> r
+r \\ d = withDict d r
+
+infixr 9 :-
+infixr 9 ⊢
+
+type (⊢) = (:-)
+
+-- | This is the type of entailment.
+--
+-- @a ':-' b@ is read as @a@ \"entails\" @b@.
+--
+-- With this we can actually build a category for 'Constraint' resolution.
+--
+-- e.g.
+--
+-- Because @'Eq' a@ is a superclass of @'Ord' a@, we can show that @'Ord' a@
+-- entails @'Eq' a@.
+--
+-- Because @instance 'Ord' a => 'Ord' [a]@ exists, we can show that @'Ord' a@
+-- entails @'Ord' [a]@ as well.
+--
+-- This relationship is captured in the ':-' entailment type here.
+--
+-- Since @p ':-' p@ and entailment composes, ':-' forms the arrows of a
+-- 'Category' of constraints. However, 'Category' only became sufficiently
+-- general to support this instance in GHC 7.8, so prior to 7.8 this instance
+-- is unavailable.
+--
+-- But due to the coherence of instance resolution in Haskell, this 'Category'
+-- has some very interesting properties. Notably, in the absence of
+-- @IncoherentInstances@, this category is \"thin\", which is to say that
+-- between any two objects (constraints) there is at most one distinguishable
+-- arrow.
+--
+-- This means that for instance, even though there are two ways to derive
+-- @'Ord' a ':-' 'Eq' [a]@, the answers from these two paths _must_ by
+-- construction be equal. This is a property that Haskell offers that is
+-- pretty much unique in the space of languages with things they call \"type
+-- classes\".
+--
+-- What are the two ways?
+--
+-- Well, we can go from @'Ord' a ':-' 'Eq' a@ via the
+-- superclass relationship, and then from @'Eq' a ':-' 'Eq' [a]@ via the
+-- instance, or we can go from @'Ord' a ':-' 'Ord' [a]@ via the instance
+-- then from @'Ord' [a] ':-' 'Eq' [a]@ through the superclass relationship
+-- and this diagram by definition must \"commute\".
+--
+-- Diagrammatically,
+--
+-- >                    Ord a
+-- >                ins /     \ cls
+-- >                   v       v
+-- >             Ord [a]     Eq a
+-- >                cls \     / ins
+-- >                     v   v
+-- >                    Eq [a]
+--
+-- This safety net ensures that pretty much anything you can write with this
+-- library is sensible and can't break any assumptions on the behalf of
+-- library authors.
+newtype a :- b = Sub (a => Dict b)
+  deriving Typeable
+
+type role (:-) nominal nominal
+
+-- TODO: _proper_ Data for @(p ':-' q)@ requires @(:-)@ to be cartesian _closed_.
+--
+-- This is admissable, but not present by default
+
+-- constraint should be instance (Typeable p, Typeable q, p |- q) => Data (p :- q)
+instance (Typeable p, Typeable q, p, q) => Data (p :- q) where
+  gfoldl _ z (Sub Dict) = z (Sub Dict)
+  toConstr _ = subConstr
+  gunfold _ z c = case constrIndex c of
+    1 -> z (Sub Dict)
+    _ -> error "gunfold"
+  dataTypeOf _ = subDataType
+
+subConstr :: Constr
+subConstr = mkConstr dictDataType "Sub" [] Prefix
+
+subDataType :: DataType
+subDataType = mkDataType "Data.Constraint.:-" [subConstr]
+
+-- | Possible since GHC 7.8, when 'Category' was made polykinded.
+instance Category (:-) where
+  id  = refl
+  (.) = trans
+
+-- | Assumes 'IncoherentInstances' doesn't exist.
+instance Eq (a :- b) where
+  _ == _ = True
+
+-- | Assumes 'IncoherentInstances' doesn't exist.
+instance Ord (a :- b) where
+  compare _ _ = EQ
+
+instance Show (a :- b) where
+  showsPrec d _ = showParen (d > 10) $ showString "Sub Dict"
+
+
+--------------------------------------------------------------------------------
+-- Constraints form a Category
+--------------------------------------------------------------------------------
+
+-- | Transitivity of entailment
+--
+-- If we view @(':-')@ as a Constraint-indexed category, then this is @('.')@
+trans :: (b :- c) -> (a :- b) -> a :- c
+trans f g = Sub $ Dict \\ f \\ g
+
+-- | Reflexivity of entailment
+--
+-- If we view @(':-')@ as a Constraint-indexed category, then this is 'id'
+refl :: a :- a
+refl = Sub Dict
+
+--------------------------------------------------------------------------------
+-- (,) is a Bifunctor
+--------------------------------------------------------------------------------
+
+-- | due to the hack for the kind of @(,)@ in the current version of GHC we can't actually
+-- make instances for @(,) :: Constraint -> Constraint -> Constraint@, but @(,)@ is a
+-- bifunctor on the category of constraints. This lets us map over both sides.
+(***) :: (a :- b) -> (c :- d) -> (a, c) :- (b, d)
+f *** g = Sub $ Dict \\ f \\ g
+
+--------------------------------------------------------------------------------
+-- Constraints are Cartesian
+--------------------------------------------------------------------------------
+
+-- | Weakening a constraint product
+--
+-- The category of constraints is Cartesian. We can forget information.
+weaken1 :: (a, b) :- a
+weaken1 = Sub Dict
+
+-- | Weakening a constraint product
+--
+-- The category of constraints is Cartesian. We can forget information.
+weaken2 :: (a, b) :- b
+weaken2 = Sub Dict
+
+strengthen1 :: Dict b -> a :- c -> a :- (b,c)
+strengthen1 d e = unmapDict (const d) &&& e
+
+strengthen2 :: Dict b -> a :- c -> a :- (c,b)
+strengthen2 d e = e &&& unmapDict (const d)
+
+-- | Contracting a constraint / diagonal morphism
+--
+-- The category of constraints is Cartesian. We can reuse information.
+contract :: a :- (a, a)
+contract = Sub Dict
+
+-- | Constraint product
+--
+-- > trans weaken1 (f &&& g) = f
+-- > trans weaken2 (f &&& g) = g
+(&&&) :: (a :- b) -> (a :- c) -> a :- (b, c)
+f &&& g = Sub $ Dict \\ f \\ g
+
+--------------------------------------------------------------------------------
+-- Initial and terminal morphisms
+--------------------------------------------------------------------------------
+
+-- | Every constraint implies truth
+--
+-- These are the terminal arrows of the category, and @()@ is the terminal object.
+--
+-- Given any constraint there is a unique entailment of the @()@ constraint from that constraint.
+top :: a :- ()
+top = Sub Dict
+
+-- | 'Any' inhabits every kind, including 'Constraint' but is uninhabited, making it impossible to define an instance.
+class Exts.Any => Bottom where
+  no :: a
+
+-- |
+-- This demonstrates the law of classical logic <http://en.wikipedia.org/wiki/Principle_of_explosion "ex falso quodlibet">
+bottom :: Bottom :- a
+bottom = Sub no
+
+--------------------------------------------------------------------------------
+-- Dict is fully faithful
+--------------------------------------------------------------------------------
+
+-- | Apply an entailment to a dictionary.
+--
+-- From a category theoretic perspective 'Dict' is a functor that maps from the category
+-- of constraints (with arrows in ':-') to the category Hask of Haskell data types.
+mapDict :: (a :- b) -> Dict a -> Dict b
+mapDict p Dict = case p of Sub q -> q
+
+-- |
+-- This functor is fully faithful, which is to say that given any function you can write
+-- @Dict a -> Dict b@ there also exists an entailment @a :- b@ in the category of constraints
+-- that you can build.
+unmapDict :: (Dict a -> Dict b) -> a :- b
+unmapDict f = Sub (f Dict)
+
+type role Dict nominal
+
+--------------------------------------------------------------------------------
+-- Reflection
+--------------------------------------------------------------------------------
+
+-- | Reify the relationship between a class and its superclass constraints as a class
+--
+-- Given a definition such as
+--
+-- @
+-- class Foo a => Bar a
+-- @
+--
+-- you can capture the relationship between 'Bar a' and its superclass 'Foo a' with
+--
+-- @
+-- instance 'Class' (Foo a) (Bar a) where 'cls' = 'Sub' 'Dict'
+-- @
+--
+-- Now the user can use 'cls :: Bar a :- Foo a'
+class Class b h | h -> b where
+  cls :: h :- b
+
+infixr 9 :=>
+-- | Reify the relationship between an instance head and its body as a class
+--
+-- Given a definition such as
+--
+-- @
+-- instance Foo a => Foo [a]
+-- @
+--
+-- you can capture the relationship between the instance head and its body with
+--
+-- @
+-- instance Foo a ':=>' Foo [a] where 'ins' = 'Sub' 'Dict'
+-- @
+class b :=> h | h -> b where
+  ins :: b :- h
+
+-- Bootstrapping
+
+instance Class () (Class b a) where cls = Sub Dict
+instance Class () (b :=> a) where cls = Sub Dict
+
+instance Class b a => () :=> Class b a where ins = Sub Dict
+instance (b :=> a) => () :=> (b :=> a) where ins = Sub Dict
+
+instance Class () () where cls = Sub Dict
+instance () :=> () where ins = Sub Dict
+
+-- Local, Prelude, Applicative, C.M.I and Data.Monoid instances
+
+-- Eq
+instance Class () (Eq a) where cls = Sub Dict
+instance () :=> Eq () where ins = Sub Dict
+instance () :=> Eq Int where ins = Sub Dict
+instance () :=> Eq Bool where ins = Sub Dict
+instance () :=> Eq Integer where ins = Sub Dict
+instance () :=> Eq Float where ins = Sub Dict
+instance () :=> Eq Double where ins = Sub Dict
+instance Eq a :=> Eq [a] where ins = Sub Dict
+instance Eq a :=> Eq (Maybe a) where ins = Sub Dict
+instance Eq a :=> Eq (Complex a) where ins = Sub Dict
+instance Eq a :=> Eq (Ratio a) where ins = Sub Dict
+instance (Eq a, Eq b) :=> Eq (a, b) where ins = Sub Dict
+instance (Eq a, Eq b) :=> Eq (Either a b) where ins = Sub Dict
+instance () :=> Eq (Dict a) where ins = Sub Dict
+instance () :=> Eq (a :- b) where ins = Sub Dict
+instance () :=> Eq Word where ins = Sub Dict
+instance Eq a :=> Eq (Identity a) where ins = Sub Dict
+#if MIN_VERSION_base(4,8,0)
+instance Eq a :=> Eq (Const a b) where ins = Sub Dict
+instance () :=> Eq Natural where ins = Sub Dict
+#endif
+
+-- Ord
+instance Class (Eq a) (Ord a) where cls = Sub Dict
+instance () :=> Ord () where ins = Sub Dict
+instance () :=> Ord Bool where ins = Sub Dict
+instance () :=> Ord Int where ins = Sub Dict
+instance ():=> Ord Integer where ins = Sub Dict
+instance () :=> Ord Float where ins = Sub Dict
+instance ():=> Ord Double where ins = Sub Dict
+instance () :=> Ord Char where ins = Sub Dict
+instance Ord a :=> Ord (Maybe a) where ins = Sub Dict
+instance Ord a :=> Ord [a] where ins = Sub Dict
+instance (Ord a, Ord b) :=> Ord (a, b) where ins = Sub Dict
+instance (Ord a, Ord b) :=> Ord (Either a b) where ins = Sub Dict
+instance Integral a :=> Ord (Ratio a) where ins = Sub Dict
+instance () :=> Ord (Dict a) where ins = Sub Dict
+instance () :=> Ord (a :- b) where ins = Sub Dict
+instance () :=> Ord Word where ins = Sub Dict
+instance Ord a :=> Ord (Identity a) where ins = Sub Dict
+#if MIN_VERSION_base(4,8,0)
+instance Ord a :=> Ord (Const a b) where ins = Sub Dict
+instance () :=> Ord Natural where ins = Sub Dict
+#endif
+
+-- Show
+instance Class () (Show a) where cls = Sub Dict
+instance () :=> Show () where ins = Sub Dict
+instance () :=> Show Bool where ins = Sub Dict
+instance () :=> Show Ordering where ins = Sub Dict
+instance () :=> Show Char where ins = Sub Dict
+instance () :=> Show Int where ins = Sub Dict
+instance Show a :=> Show (Complex a) where ins = Sub Dict
+instance Show a :=> Show [a] where ins = Sub Dict
+instance Show a :=> Show (Maybe a) where ins = Sub Dict
+instance (Show a, Show b) :=> Show (a, b) where ins = Sub Dict
+instance (Show a, Show b) :=> Show (Either a b) where ins = Sub Dict
+instance (Integral a, Show a) :=> Show (Ratio a) where ins = Sub Dict
+instance () :=> Show (Dict a) where ins = Sub Dict
+instance () :=> Show (a :- b) where ins = Sub Dict
+instance () :=> Show Word where ins = Sub Dict
+instance Show a :=> Show (Identity a) where ins = Sub Dict
+#if MIN_VERSION_base(4,8,0)
+instance Show a :=> Show (Const a b) where ins = Sub Dict
+instance () :=> Show Natural where ins = Sub Dict
+#endif
+
+-- Read
+instance Class () (Read a) where cls = Sub Dict
+instance () :=> Read () where ins = Sub Dict
+instance () :=> Read Bool where ins = Sub Dict
+instance () :=> Read Ordering where ins = Sub Dict
+instance () :=> Read Char where ins = Sub Dict
+instance () :=> Read Int where ins = Sub Dict
+instance Read a :=> Read (Complex a) where ins = Sub Dict
+instance Read a :=> Read [a] where ins = Sub Dict
+instance Read a :=> Read (Maybe a) where ins = Sub Dict
+instance (Read a, Read b) :=> Read (a, b) where ins = Sub Dict
+instance (Read a, Read b) :=> Read (Either a b) where ins = Sub Dict
+instance (Integral a, Read a) :=> Read (Ratio a) where ins = Sub Dict
+instance () :=> Read Word where ins = Sub Dict
+instance Read a :=> Read (Identity a) where ins = Sub Dict
+#if MIN_VERSION_base(4,8,0)
+instance Read a :=> Read (Const a b) where ins = Sub Dict
+instance () :=> Read Natural where ins = Sub Dict
+#endif
+
+-- Enum
+instance Class () (Enum a) where cls = Sub Dict
+instance () :=> Enum () where ins = Sub Dict
+instance () :=> Enum Bool where ins = Sub Dict
+instance () :=> Enum Ordering where ins = Sub Dict
+instance () :=> Enum Char where ins = Sub Dict
+instance () :=> Enum Int where ins = Sub Dict
+instance () :=> Enum Integer where ins = Sub Dict
+instance () :=> Enum Float where ins = Sub Dict
+instance () :=> Enum Double where ins = Sub Dict
+instance Integral a :=> Enum (Ratio a) where ins = Sub Dict
+instance () :=> Enum Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Enum a :=> Enum (Identity a) where ins = Sub Dict
+instance Enum a :=> Enum (Const a b) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,8,0)
+instance () :=> Enum Natural where ins = Sub Dict
+#endif
+
+-- Bounded
+instance Class () (Bounded a) where cls = Sub Dict
+instance () :=> Bounded () where ins = Sub Dict
+instance () :=> Bounded Ordering where ins = Sub Dict
+instance () :=> Bounded Bool where ins = Sub Dict
+instance () :=> Bounded Int where ins = Sub Dict
+instance () :=> Bounded Char where ins = Sub Dict
+instance (Bounded a, Bounded b) :=> Bounded (a,b) where ins = Sub Dict
+instance () :=> Bounded Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Bounded a :=> Bounded (Identity a) where ins = Sub Dict
+instance Bounded a :=> Bounded (Const a b) where ins = Sub Dict
+#endif
+
+-- Num
+instance Class () (Num a) where cls = Sub Dict
+instance () :=> Num Int where ins = Sub Dict
+instance () :=> Num Integer where ins = Sub Dict
+instance () :=> Num Float where ins = Sub Dict
+instance () :=> Num Double where ins = Sub Dict
+instance RealFloat a :=> Num (Complex a) where ins = Sub Dict
+instance Integral a :=> Num (Ratio a) where ins = Sub Dict
+instance () :=> Num Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Num a :=> Num (Identity a) where ins = Sub Dict
+instance Num a :=> Num (Const a b) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,8,0)
+instance () :=> Num Natural where ins = Sub Dict
+#endif
+
+-- Real
+instance Class (Num a, Ord a) (Real a) where cls = Sub Dict
+instance () :=> Real Int where ins = Sub Dict
+instance () :=> Real Integer where ins = Sub Dict
+instance () :=> Real Float where ins = Sub Dict
+instance () :=> Real Double where ins = Sub Dict
+instance Integral a :=> Real (Ratio a) where ins = Sub Dict
+instance () :=> Real Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Real a :=> Real (Identity a) where ins = Sub Dict
+instance Real a :=> Real (Const a b) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,8,0)
+instance () :=> Real Natural where ins = Sub Dict
+#endif
+
+-- Integral
+instance Class (Real a, Enum a) (Integral a) where cls = Sub Dict
+instance () :=> Integral Int where ins = Sub Dict
+instance () :=> Integral Integer where ins = Sub Dict
+instance () :=> Integral Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Integral a :=> Integral (Identity a) where ins = Sub Dict
+instance Integral a :=> Integral (Const a b) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,8,0)
+instance () :=> Integral Natural where ins = Sub Dict
+#endif
+
+-- Bits
+instance Class (Eq a) (Bits a) where cls = Sub Dict
+instance () :=> Bits Bool where ins = Sub Dict
+instance () :=> Bits Int where ins = Sub Dict
+instance () :=> Bits Integer where ins = Sub Dict
+instance () :=> Bits Word where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Bits a :=> Bits (Identity a) where ins = Sub Dict
+instance Bits a :=> Bits (Const a b) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,8,0)
+instance () :=> Bits Natural where ins = Sub Dict
+#endif
+
+-- Fractional
+instance Class (Num a) (Fractional a) where cls = Sub Dict
+instance () :=> Fractional Float where ins = Sub Dict
+instance () :=> Fractional Double where ins = Sub Dict
+instance RealFloat a :=> Fractional (Complex a) where ins = Sub Dict
+instance Integral a :=> Fractional (Ratio a) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Fractional a :=> Fractional (Identity a) where ins = Sub Dict
+instance Fractional a :=> Fractional (Const a b) where ins = Sub Dict
+#endif
+
+-- Floating
+instance Class (Fractional a) (Floating a) where cls = Sub Dict
+instance () :=> Floating Float where ins = Sub Dict
+instance () :=> Floating Double where ins = Sub Dict
+instance RealFloat a :=> Floating (Complex a) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Floating a :=> Floating (Identity a) where ins = Sub Dict
+instance Floating a :=> Floating (Const a b) where ins = Sub Dict
+#endif
+
+-- RealFrac
+instance Class (Real a, Fractional a) (RealFrac a) where cls = Sub Dict
+instance () :=> RealFrac Float where ins = Sub Dict
+instance () :=> RealFrac Double where ins = Sub Dict
+instance Integral a :=> RealFrac (Ratio a) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance RealFrac a :=> RealFrac (Identity a) where ins = Sub Dict
+instance RealFrac a :=> RealFrac (Const a b) where ins = Sub Dict
+#endif
+
+-- RealFloat
+instance Class (RealFrac a, Floating a) (RealFloat a) where cls = Sub Dict
+instance () :=> RealFloat Float where ins = Sub Dict
+instance () :=> RealFloat Double where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance RealFloat a :=> RealFloat (Identity a) where ins = Sub Dict
+instance RealFloat a :=> RealFloat (Const a b) where ins = Sub Dict
+#endif
+
+-- Semigroup
+instance Class () (Semigroup a) where cls = Sub Dict
+instance () :=> Semigroup () where ins = Sub Dict
+instance () :=> Semigroup Ordering where ins = Sub Dict
+instance () :=> Semigroup [a] where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Maybe a) where ins = Sub Dict
+instance (Semigroup a, Semigroup b) :=> Semigroup (a, b) where ins = Sub Dict
+instance Semigroup a :=> Semigroup (Const a b) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Semigroup a :=> Semigroup (Identity a) where ins = Sub Dict
+#endif
+#if MIN_VERSION_base(4,10,0)
+instance Semigroup a :=> Semigroup (IO a) where ins = Sub Dict
+#endif
+
+-- Monoid
+#if MIN_VERSION_base(4,11,0)
+instance Class (Semigroup a) (Monoid a) where cls = Sub Dict
+#else
+instance Class () (Monoid a) where cls = Sub Dict
+#endif
+instance () :=> Monoid () where ins = Sub Dict
+instance () :=> Monoid Ordering where ins = Sub Dict
+instance () :=> Monoid [a] where ins = Sub Dict
+instance Monoid a :=> Monoid (Maybe a) where ins = Sub Dict
+instance (Monoid a, Monoid b) :=> Monoid (a, b) where ins = Sub Dict
+instance Monoid a :=> Monoid (Const a b) where ins = Sub Dict
+#if MIN_VERSION_base(4,9,0)
+instance Monoid a :=> Monoid (Identity a) where ins = Sub Dict
+instance Monoid a :=> Monoid (IO a) where ins = Sub Dict
+#endif
+
+-- Functor
+instance Class () (Functor f) where cls = Sub Dict
+instance () :=> Functor [] where ins = Sub Dict
+instance () :=> Functor Maybe where ins = Sub Dict
+instance () :=> Functor (Either a) where ins = Sub Dict
+instance () :=> Functor ((->) a) where ins = Sub Dict
+instance () :=> Functor ((,) a) where ins = Sub Dict
+instance () :=> Functor IO where ins = Sub Dict
+instance Monad m :=> Functor (WrappedMonad m) where ins = Sub Dict
+instance () :=> Functor Identity where ins = Sub Dict
+instance () :=> Functor (Const a) where ins = Sub Dict
+
+-- Applicative
+instance Class (Functor f) (Applicative f) where cls = Sub Dict
+instance () :=> Applicative [] where ins = Sub Dict
+instance () :=> Applicative Maybe where ins = Sub Dict
+instance () :=> Applicative (Either a) where ins = Sub Dict
+instance () :=> Applicative ((->)a) where ins = Sub Dict
+instance () :=> Applicative IO where ins = Sub Dict
+instance Monoid a :=> Applicative ((,)a) where ins = Sub Dict
+instance Monoid a :=> Applicative (Const a) where ins = Sub Dict
+instance Monad m :=> Applicative (WrappedMonad m) where ins = Sub Dict
+
+-- Alternative
+instance Class (Applicative f) (Alternative f) where cls = Sub Dict
+instance () :=> Alternative [] where ins = Sub Dict
+instance () :=> Alternative Maybe where ins = Sub Dict
+instance MonadPlus m :=> Alternative (WrappedMonad m) where ins = Sub Dict
+
+-- Monad
+#if MIN_VERSION_base(4,8,0)
+instance Class (Applicative f) (Monad f) where cls = Sub Dict
+#else
+instance Class () (Monad f) where cls = Sub Dict
+#endif
+instance () :=> Monad [] where ins = Sub Dict
+instance () :=> Monad ((->) a) where ins = Sub Dict
+instance () :=> Monad (Either a) where ins = Sub Dict
+instance () :=> Monad IO where ins = Sub Dict
+instance () :=> Monad Identity where ins = Sub Dict
+
+-- MonadPlus
+#if MIN_VERSION_base(4,8,0)
+instance Class (Monad f, Alternative f) (MonadPlus f) where cls = Sub Dict
+#else
+instance Class (Monad f) (MonadPlus f) where cls = Sub Dict
+#endif
+instance () :=> MonadPlus [] where ins = Sub Dict
+instance () :=> MonadPlus Maybe where ins = Sub Dict
+
+--------------------------------------------------------------------------------
+-- UndecidableInstances
+--------------------------------------------------------------------------------
+
+instance a :=> Enum (Dict a) where ins = Sub Dict
+instance a => Enum (Dict a) where
+  toEnum _ = Dict
+  fromEnum Dict = 0
+
+instance a :=> Bounded (Dict a) where ins = Sub Dict
+instance a => Bounded (Dict a) where
+  minBound = Dict
+  maxBound = Dict
+
+instance a :=> Read (Dict a) where ins = Sub Dict
+deriving instance a => Read (Dict a)
+
+instance () :=> Semigroup (Dict a) where ins = Sub Dict
+instance Semigroup (Dict a) where
+  Dict <> Dict = Dict
+
+instance a :=> Monoid (Dict a) where ins = Sub Dict
+instance a => Monoid (Dict a) where
+#if !(MIN_VERSION_base(4,11,0))
+  mappend = (<>)
+#endif
+  mempty = Dict
+ src-constraints/Data/Constraint/Unsafe.hs view
@@ -0,0 +1,72 @@+{-
+Copyright 2011-2015 Edward Kmett
+
+All rights reserved.
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions
+are met:
+
+1. Redistributions of source code must retain the above copyright
+   notice, this list of conditions and the following disclaimer.
+
+2. 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.
+
+THIS SOFTWARE IS PROVIDED BY THE AUTHORS ``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 AUTHORS 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.
+ -}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Rank2Types #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE Unsafe #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Constraint.Unsafe
+-- Copyright   :  (C) 2011-2015 Edward Kmett
+-- License     :  BSD-style (see the file LICENSE)
+--
+-- Stability   :  experimental
+-- Portability :  non-portable
+--
+-- This module is taken from
+-- <https://github.com/ekmett/constraints/blob/963c0e904ad48a5cec29a0cb649622d8c1872af4/src/Data/Constraint/Unsafe.hs constraints:Data.Constraint.Unsafe>
+-- A few things have been cut from the module.
+--
+----------------------------------------------------------------------------
+module Data.Constraint.Unsafe
+  ( Coercible
+  , unsafeCoerceConstraint
+  , unsafeDerive
+  , unsafeUnderive
+  ) where
+
+import Data.Coerce
+import Data.Constraint
+import Unsafe.Coerce
+
+-- | Coerce a dictionary unsafely from one type to another
+unsafeCoerceConstraint :: a :- b
+unsafeCoerceConstraint = unsafeCoerce refl
+
+-- | Coerce a dictionary unsafely from one type to a newtype of that type
+unsafeDerive :: Coercible n o => (o -> n) -> t o :- t n
+unsafeDerive _ = unsafeCoerceConstraint
+
+-- | Coerce a dictionary unsafely from a newtype of a type to the base type
+unsafeUnderive :: Coercible n o => (o -> n) -> t n :- t o
+unsafeUnderive _ = unsafeCoerceConstraint
+ src/Data/Constraint/Bare.hs view
@@ -0,0 +1,63 @@+{-# LANGUAGE CPP             #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds       #-}
+{-# LANGUAGE GADTs           #-}
+{-# LANGUAGE KindSignatures  #-}
+{-# LANGUAGE MagicHash       #-}
+{-# LANGUAGE PatternSynonyms #-}
+{-# LANGUAGE RankNTypes      #-}
+{-# LANGUAGE ViewPatterns    #-}
+-----------------------------------------------------------------------------
+-- |
+-- Module      :  Data.Constraint.Bare
+-- Copyright   :  (c) 2019 Artem Chirkin
+-- License     :  BSD3
+-- Portability :  non-portable
+--
+-- Extract a Constraint from a Dict to manipulate it as a plain value.
+-- It is supposed to be used in compiler plugins
+--   -- to move around instances of type classes.
+--
+-----------------------------------------------------------------------------
+module Data.Constraint.Bare
+  ( BareConstraint, pattern DictValue
+  , dictToBare, bareToDict
+  ) where
+
+
+import Data.Constraint (Dict (..))
+import GHC.Base        (Constraint, Type, unsafeCoerce#)
+
+-- | An unsafeCoerced pointer to a Constraint, such as a class function dictionary.
+data BareConstraint :: Constraint -> Type
+
+-- | Extract the constraint inside the Dict GADT as if it was
+--   an ordinary value of kind `Type`.
+--
+--   It exploits the feature of the GHC core language
+--    -- representing constraints as ordinary type arguments of a function.
+--   Thus, I unsafeCoerce between a function with one argument and a function
+--    with no arguments and one constraint.
+--
+--   This pattern has never been tested with multiple constraints.
+pattern DictValue :: BareConstraint c -> Dict c
+pattern DictValue c <- (dictToBare -> c)
+  where
+    DictValue c = bareToDict c
+
+#if __GLASGOW_HASKELL__ >= 802
+{-# COMPLETE DictValue #-}
+#endif
+
+-- | Extract a `Constraint` from a `Dict`
+dictToBare :: Dict c -> BareConstraint c
+dictToBare Dict = case unsafeCoerce# id of MagicBC c -> c
+{-# INLINE dictToBare #-}
+
+-- | Wrap a `Constraint` into a `Dict`
+bareToDict :: BareConstraint c -> Dict c
+bareToDict = unsafeCoerce# (MagicDi Dict)
+{-# INLINE bareToDict #-}
+
+newtype MagicDi c = MagicDi (c => Dict c)
+newtype MagicBC c = MagicBC (c => BareConstraint c)
+ src/Data/Constraint/Deriving.hs view
@@ -0,0 +1,78 @@+{-# LANGUAGE CPP #-}
+module Data.Constraint.Deriving
+  ( plugin
+    -- * DeriveAll pass
+  , DeriveAll (..)
+  , DeriveContext
+    -- * ToInstance pass
+  , ToInstance (..)
+  , OverlapMode (..)
+  ) where
+
+
+
+import Data.List  (sortOn)
+import GhcPlugins hiding (OverlapMode (..), overlapMode)
+import InstEnv    (is_tys, is_cls)
+import Type       (tyConAppTyCon_maybe)
+
+import Data.Constraint.Deriving.DeriveAll
+import Data.Constraint.Deriving.ToInstance
+
+
+
+-- | To use the plugin, add
+--
+-- @
+-- {\-\# OPTIONS_GHC -fplugin Data.Constraint.Deriving \#-\}
+-- @
+--
+-- to the header of your file.
+--
+-- For debugging, add a plugin option @dump-instances@
+--
+-- @
+-- {\-\# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances \#-\}
+-- @
+--
+-- to the header of your file; it will print all instances declared in the module
+-- (hand-written and auto-generated).
+--
+plugin :: Plugin
+plugin = defaultPlugin
+  { installCoreToDos = install
+#if MIN_VERSION_ghc(8,6,0)
+  , pluginRecompile = purePlugin
+#endif
+  }
+
+install :: [CommandLineOption] -> [CoreToDo] -> CoreM [CoreToDo]
+install cmdopts todo = do
+    eref <- initCorePluginEnv
+    return ( deriveAllPass eref
+           : toInstancePass eref
+           : if elem "dump-instances" cmdopts
+             then dumpInstances:todo
+             else todo
+           )
+
+
+-- | Just print all instance signatures in this module
+dumpInstances :: CoreToDo
+dumpInstances = CoreDoPluginPass "Data.Constraint.Deriving.DumpInstances"
+              $ \guts -> guts <$ go (mg_insts guts)
+  where
+    locdoc i = ( ( getOccString $ is_cls i
+                 , map (fmap getOccString . tyConAppTyCon_maybe)
+                   $ is_tys i
+                 ), ppr i)
+    go is = do
+      let is' = sortOn fst $ map locdoc is
+      putMsg $
+        blankLine
+        $+$
+        hang
+          (text "============ Class instances declared in this module ============")
+          2 (vcat $ map snd is')
+        $+$
+        blankLine
+ src/Data/Constraint/Deriving/CorePluginM.hs view
@@ -0,0 +1,630 @@+{-# LANGUAGE CPP                 #-}
+{-# LANGUAGE DeriveDataTypeable  #-}
+{-# LANGUAGE FlexibleContexts    #-}
+{-# LANGUAGE LambdaCase          #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+#if __GLASGOW_HASKELL__ < 802
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+#endif
+module Data.Constraint.Deriving.CorePluginM
+  ( CorePluginM (), runCorePluginM
+  , CorePluginEnv (), CorePluginEnvRef, initCorePluginEnv
+  , liftCoreM, runTcM, liftIO, lookupName
+    -- * Error handling
+  , try, exception
+    -- * Accessing read-only on-demand variables
+  , ask
+  , tyConDict, tyConBareConstraint, tyConDeriveContext
+  , funDictToBare, tyEmptyConstraint, classTypeEq
+    -- * Reporting
+  , pluginWarning, pluginLocatedWarning
+  , pluginError, pluginLocatedError
+    -- * Tools
+  , newName, newTyVar, freshenTyVar
+  , bullet, isConstraintKind, getModuleAnns
+  , filterAvails
+  , recMatchTyKi, replaceTypeOccurrences
+  , OverlapMode (..), toOverlapFlag
+  , lookupClsInsts, getInstEnvs
+    -- * Debugging
+  , pluginDebug, pluginTrace
+  , HasCallStack
+  ) where
+
+import qualified Avail
+import           Class               (Class)
+import           Control.Applicative ((<|>))
+import           Control.Monad       (join)
+import           Data.Data           (Data, typeRep)
+import           Data.IORef          (IORef, modifyIORef', newIORef, readIORef)
+import           Data.Maybe          (catMaybes)
+import           Data.Monoid         (First (..))
+import           Data.Proxy          (Proxy (..))
+import qualified ErrUtils
+import qualified Finder
+import           GhcPlugins          hiding (OverlapMode (..), overlapMode,
+                                      (<>))
+import qualified GhcPlugins
+import qualified IfaceEnv
+import           InstEnv             (InstEnv, InstEnvs)
+import qualified InstEnv
+import qualified LoadIface
+import           MonadUtils          (MonadIO (..))
+import           TcRnMonad           (getEps, initTc)
+import           TcRnTypes           (TcM)
+import qualified Unify
+#if __GLASGOW_HASKELL__ < 806
+import qualified Kind      (isConstraintKind)
+import qualified TcRnMonad (initTcForLookup)
+#endif
+#if __GLASGOW_HASKELL__ < 802
+import GHC.Stack (HasCallStack)
+#endif
+#if PLUGIN_DEBUG
+import GHC.Stack (withFrozenCallStack)
+#endif
+
+-- | Since I do not have access to the guts of CoreM monad,
+--   I implement a wrapper on top of it here.
+--
+--   It provides two pieces of functionality:
+--
+--     * Possibility to fail a computation
+--       (to show a nice error to a user and continue the work if possible);
+--
+--     * An environment with things that computed on demand, once at most.
+--
+newtype CorePluginM a = CorePluginM
+  { runCorePluginM :: IORef CorePluginEnv -> CoreM (Maybe a) }
+
+instance Functor CorePluginM where
+  fmap f m = CorePluginM $ fmap (fmap f) . runCorePluginM m
+
+instance Applicative CorePluginM where
+  pure = CorePluginM . const . pure . Just
+  mf <*> ma = CorePluginM $ \e -> (<*>) <$> runCorePluginM mf e <*> runCorePluginM ma e
+
+instance Monad CorePluginM where
+  return = pure
+  ma >>= k = CorePluginM $ \e -> runCorePluginM ma e >>= \case
+    Nothing -> pure Nothing
+    Just a  -> runCorePluginM (k a) e
+
+instance MonadIO CorePluginM where
+  liftIO = liftCoreM . liftIO
+
+instance MonadThings CorePluginM where
+  lookupThing = liftCoreM . lookupThing
+
+instance MonadUnique CorePluginM where
+  getUniqueSupplyM = CorePluginM $ const $ Just <$> getUniqueSupplyM
+
+
+-- | Wrap CoreM action
+liftCoreM :: CoreM a -> CorePluginM a
+liftCoreM = CorePluginM . const . fmap Just
+
+-- | Synonym for `fail`
+exception :: CorePluginM a
+exception = CorePluginM $ const $ pure Nothing
+
+-- | Return `Nothing` if the computation fails
+try :: CorePluginM a -> CorePluginM (Maybe a)
+try m = CorePluginM $ fmap Just . runCorePluginM m
+
+-- | Reference to the plugin environment variables.
+type CorePluginEnvRef = IORef CorePluginEnv
+
+-- | Plugin environment
+--
+--   Its components are supposed to be computed at most once, when they are needed.
+data CorePluginEnv = CorePluginEnv
+  { modConstraint       :: CorePluginM Module
+  , modConstraintBare   :: CorePluginM Module
+  , modDeriveAll        :: CorePluginM Module
+  , modToInstance       :: CorePluginM Module
+  , modDataTypeEquality :: CorePluginM Module
+  , tyConDict           :: CorePluginM TyCon
+  , tyConBareConstraint :: CorePluginM TyCon
+  , tyConDeriveContext  :: CorePluginM TyCon
+  , funDictToBare       :: CorePluginM Id
+  , tyEmptyConstraint   :: CorePluginM Type
+  , classTypeEq         :: CorePluginM Class
+  , globalInstEnv       :: CorePluginM InstEnv
+  }
+
+-- | Ask a field of the CorePluginEnv environment.
+ask :: (CorePluginEnv -> CorePluginM a) -> CorePluginM a
+ask f = join $ CorePluginM $ liftIO . fmap (Just . f) . readIORef
+
+-- | Init the `CorePluginM` environment and save it to IORef.
+initCorePluginEnv :: CoreM (IORef CorePluginEnv)
+initCorePluginEnv = do
+  env <- liftIO $ newIORef defCorePluginEnv
+  -- need to force globalInstEnv as early as possible to make sure
+  -- that ExternalPackageState var is not yet contaminated with
+  -- many unrelated modules.
+  gie <- runCorePluginM (ask globalInstEnv) env
+  seq gie $ return env
+
+
+-- | Lookup necessary environment components on demand.
+defCorePluginEnv :: CorePluginEnv
+defCorePluginEnv = CorePluginEnv
+    { modConstraint = do
+        mm <- try $ lookupModule mnConstraint [pnConstraintsDeriving, pnConstraints]
+        saveAndReturn mm $ \a e -> e { modConstraint = a }
+
+    , modConstraintBare = do
+        mm <- try $ lookupModule mnConstraintBare [pnConstraintsDeriving]
+        saveAndReturn mm $ \a e -> e { modConstraintBare = a }
+
+    , modDeriveAll = do
+        mm <- try $ lookupModule mnDeriveAll [pnConstraintsDeriving]
+        saveAndReturn mm $ \a e -> e { modDeriveAll = a }
+
+    , modToInstance = do
+        mm <- try $ lookupModule mnToInstance [pnConstraintsDeriving]
+        saveAndReturn mm $ \a e -> e { modToInstance = a }
+
+    , modDataTypeEquality = do
+        mm <- try $ lookupModule mnDataTypeEquality [pnBase]
+        saveAndReturn mm $ \a e -> e { modDataTypeEquality = a }
+
+    , tyConDict = do
+        m <- ask modConstraint
+        mtc <- try $ lookupName m tnDict >>= lookupTyCon
+        saveAndReturn mtc $ \a e -> e { tyConDict = a }
+
+    , tyConBareConstraint = do
+        m <- ask modConstraintBare
+        mtc <- try $ lookupName m tnBareConstraint >>= lookupTyCon
+        saveAndReturn mtc $ \a e -> e { tyConBareConstraint = a }
+
+    , tyConDeriveContext = do
+        m <- ask modDeriveAll
+        mtc <- try $ lookupName m tnDeriveContext >>= lookupTyCon
+        saveAndReturn mtc $ \a e -> e { tyConDeriveContext = a }
+
+    , funDictToBare = do
+        m <- ask modConstraintBare
+        mf <- try $ lookupName m vnDictToBare >>= lookupId
+        saveAndReturn mf $ \a e -> e { funDictToBare = a }
+
+    , tyEmptyConstraint = do
+        ec <- flip mkTyConApp [] <$> lookupTyCon (cTupleTyConName 0)
+        saveAndReturn (Just ec) $ \a e -> e { tyEmptyConstraint = a }
+
+    , classTypeEq = do
+        m <- ask modDataTypeEquality
+        mc <- try $ lookupName m cnTypeEq >>= lookupThing >>= \case
+          ATyCon tc | Just cls <- tyConClass_maybe tc
+            -> return cls
+          _ -> exception
+        saveAndReturn mc $ \a e -> e { classTypeEq = a }
+
+    , globalInstEnv = do
+        hscEnv <- liftCoreM getHscEnv
+        mn <- moduleName <$> liftCoreM getModule
+
+        mdesc
+          <- case [ m | m <- mgModSummaries $ hsc_mod_graph hscEnv
+                      , ms_mod_name m == mn
+                      , not (isBootSummary m) ] of
+          []   -> pluginError $ hsep
+                  [ text "Could not find"
+                  , ppr mn
+                  , text "in the module graph."
+                  ]
+          [md] -> return md
+          _    -> pluginError $ hsep
+                  [ text "Found multiple modules"
+                  , ppr mn
+                  , text "in the module graph."
+                  ]
+        -- direct module dependencies
+        modsDirect <- fmap catMaybes
+          . traverse (lookupDep hscEnv)
+          $ ms_srcimps mdesc ++ ms_textual_imps mdesc
+        let -- direct dependencies; must be in the explicit depenencies anyway
+            mSetDirect = mkUniqSet $ filter notMyOwn modsDirect
+            -- Modules that we definitely need to look through,
+            -- even if they are from other, hidden packages
+            reexportedDeps i = mkUniqSet $ do
+              a@Avail.AvailTC{} <- mi_exports i
+              let m = nameModule $ Avail.availName a
+              [ m | m /= mi_module i, notMyOwn m]
+            -- Load reexportedDeps recursively.
+            -- This enumerate all modules that export some type constructors
+            -- visible from the current module;
+            -- this includes our base types and also all classes in scope.
+            loadRec ms = do
+              ifs <- traverse (LoadIface.loadModuleInterface reason)
+                      $ backToList ms
+              let ms' = foldr (unionUniqSets . reexportedDeps) ms ifs
+              if isEmptyUniqSet $ ms' `minusUniqSet` ms
+              then return ms
+              else loadRec ms'
+        gie <- runTcM $ do
+          mods <- backToList <$> loadRec mSetDirect
+          LoadIface.loadModuleInterfaces reason mods
+          eps_inst_env <$> getEps
+        saveAndReturn (Just gie) $ \a e -> e { globalInstEnv = a }
+
+    }
+  where
+    saveAndReturn Nothing  f = CorePluginM $ \eref ->
+      Nothing <$ liftIO (modifyIORef' eref $ f exception)
+    saveAndReturn (Just x) f = CorePluginM $ \eref ->
+      Just x  <$ liftIO (modifyIORef' eref $ f (pure x))
+    maybeFound (Found _ m) = Just m
+    maybeFound _           = Nothing
+    lookupDep hsce (mpn, mn)
+      = maybeFound <$>
+        liftIO (Finder.findImportedModule hsce (unLoc mn) mpn)
+    reason = text $ "Constraints.Deriving.CorePluginM "
+                               ++ "itinialization of global InstEnv"
+    -- Ignore my own modules: they do not contain any classes.
+    notMyOwn m = moduleNameString (moduleName m) `notElem`
+      [ "Data.Constraint.Deriving"
+      , "Data.Constraint.Deriving.DeriveAll"
+      , "Data.Constraint.Deriving.ToInstance"
+      , "Data.Constraint.Deriving.ToInstance"
+      , "Data.Constraint.Deriving.CorePluginM"
+      ]
+#if __GLASGOW_HASKELL__ < 804
+    mgModSummaries = id
+#endif
+#if __GLASGOW_HASKELL__ >= 802
+    backToList = nonDetEltsUniqSet
+#else
+    backToList = uniqSetToList
+#endif
+
+
+lookupName :: Module -> OccName -> CorePluginM Name
+lookupName m occn = do
+    hscEnv <- liftCoreM getHscEnv
+    liftIO
+#if __GLASGOW_HASKELL__ < 806
+        $ TcRnMonad.initTcForLookup hscEnv
+        $ IfaceEnv.lookupOrig m occn
+#else
+        $ IfaceEnv.lookupOrigIO hscEnv m occn
+#endif
+
+runTcM :: TcM a -> CorePluginM a
+runTcM mx = do
+  hsce <- liftCoreM getHscEnv
+  modu <- liftCoreM getModule
+  let sp = realSrcLocSpan $ mkRealSrcLoc (fsLit "<CorePluginM.runTcM>") 1 1
+  ((warns, errs), my) <- liftIO $ initTc hsce HsSrcFile False modu sp mx
+  mapM_ pluginWarning $ ErrUtils.pprErrMsgBagWithLoc warns
+  case my of
+    Nothing ->
+      let f []     = pluginError $ text "runTcM failed"
+          f [x]    = pluginError x
+          f (x:xs) = pluginWarning x >> f xs
+      in f $ ErrUtils.pprErrMsgBagWithLoc errs
+    Just y  -> do
+      mapM_ pluginWarning $ ErrUtils.pprErrMsgBagWithLoc errs
+      return y
+
+-- Made this similar to tcRnGetInfo
+--   and a hidden function lookupInsts used there
+lookupClsInsts :: InstEnvs -> TyCon -> [InstEnv.ClsInst]
+lookupClsInsts ie tc =
+  [ ispec        -- Search all
+  | ispec <- InstEnv.instEnvElts (InstEnv.ie_local  ie)
+          ++ InstEnv.instEnvElts (InstEnv.ie_global ie)
+  , InstEnv.instIsVisible (InstEnv.ie_visible ie) ispec
+  , tyConName tc `elemNameSet` InstEnv.orphNamesOfClsInst ispec
+  ]
+
+getInstEnvs :: ModGuts
+            -> CorePluginM InstEnv.InstEnvs
+getInstEnvs guts = do
+  globalInsts <- ask globalInstEnv
+  return $ InstEnv.InstEnvs
+    { InstEnv.ie_global  = globalInsts
+    , InstEnv.ie_local   = mg_inst_env guts
+    , InstEnv.ie_visible = mkModuleSet . dep_orphs $ mg_deps guts
+    }
+
+lookupModule :: ModuleName
+             -> [FastString]
+             -> CorePluginM Module
+lookupModule mdName pkgs = do
+    hscEnv <- liftCoreM getHscEnv
+    go hscEnv $ map Just pkgs ++ [Just (fsLit "this"), Nothing]
+  where
+    go _ [] = pluginError $ hsep [ text "Could not find module", ppr mdName]
+    go he (x:xs) = findIt he x >>= \case
+      Nothing -> go he xs
+      Just md -> return md
+
+    findIt he = fmap getIt . liftIO . Finder.findImportedModule he mdName
+    getIt (Found _ md)                = Just md
+    getIt (FoundMultiple ((md, _):_)) = Just md
+    getIt _                           = Nothing
+
+
+-- | Generate new unique type variable
+newTyVar :: Kind -> CorePluginM TyVar
+newTyVar k = flip mkTyVar k <$> newName tvName "gen"
+
+-- | Assign a new unique to a type variable;
+--   also assign a whole new name if the input is a wildcard.
+freshenTyVar :: TyVar -> CorePluginM TyVar
+freshenTyVar tv = do
+    u <- getUniqueM
+    nn <-
+      if isInternalName n
+      then return $ mkDerivedInternalName (repOccN (show u)) u n
+      else do
+        md <- liftCoreM getModule
+        loc <- liftCoreM getSrcSpanM
+        return $ mkExternalName u md (repOccN (show u) on) loc
+    return $ mkTyVar nn k
+  where
+    n = tyVarName tv
+    k = tyVarKind tv
+    on = nameOccName n
+    repOccN s oc = case occNameString oc of
+      "_" -> mkOccName (occNameSpace oc) ("fresh_" ++ s)
+      _   -> on
+
+
+
+-- | Generate new unique name
+newName :: NameSpace -> String -> CorePluginM Name
+newName nspace nameStr = do
+    md <- liftCoreM getModule
+    loc <- liftCoreM getSrcSpanM
+    u <- getUniqueM
+    return $ mkExternalName u md occname loc
+  where
+    occname = mkOccName nspace nameStr
+
+
+pluginError :: SDoc -> CorePluginM a
+pluginError msg
+  = pluginProblemMsg Nothing ErrUtils.SevError msg >> exception
+
+pluginLocatedError :: SrcSpan -> SDoc -> CorePluginM a
+pluginLocatedError loc msg
+  = pluginProblemMsg (Just loc) ErrUtils.SevError msg >> exception
+
+pluginWarning :: SDoc -> CorePluginM ()
+pluginWarning = pluginProblemMsg Nothing ErrUtils.SevWarning
+
+pluginLocatedWarning :: SrcSpan -> SDoc -> CorePluginM ()
+pluginLocatedWarning loc = pluginProblemMsg (Just loc) ErrUtils.SevWarning
+
+pluginDebug :: SDoc -> CorePluginM ()
+#if PLUGIN_DEBUG
+pluginDebug = pluginProblemMsg Nothing ErrUtils.SevDump
+#else
+pluginDebug = const (pure ())
+#endif
+{-# INLINE pluginDebug #-}
+
+pluginTrace :: HasCallStack => SDoc -> a -> a
+#if PLUGIN_DEBUG
+pluginTrace = withFrozenCallStack pprSTrace
+#else
+pluginTrace = const id
+#endif
+{-# INLINE pluginTrace #-}
+
+
+pluginProblemMsg :: Maybe SrcSpan
+                 -> ErrUtils.Severity
+                 -> SDoc
+                 -> CorePluginM ()
+pluginProblemMsg mspan sev msg = do
+  dflags <- liftCoreM getDynFlags
+  loc    <- case mspan of
+    Just sp -> pure sp
+    Nothing -> liftCoreM getSrcSpanM
+  unqual <- liftCoreM getPrintUnqualified
+  liftIO $ putLogMsg
+    dflags NoReason sev loc (mkErrStyle dflags unqual) msg
+
+#if __GLASGOW_HASKELL__ < 802
+putLogMsg :: DynFlags -> WarnReason -> ErrUtils.Severity
+          -> SrcSpan -> PprStyle -> SDoc -> IO ()
+putLogMsg dflags = log_action dflags dflags
+#endif
+
+filterAvails :: (Name -> Bool) -> [Avail.AvailInfo] -> [Avail.AvailInfo]
+#if __GLASGOW_HASKELL__ < 802
+filterAvails _    [] = []
+filterAvails keep (a:as) = case go a of
+    Nothing -> filterAvails keep as
+    Just fa -> fa : filterAvails keep as
+  where
+    go x@(Avail.Avail _ n)
+      | keep n    = Just x
+      | otherwise = Nothing
+    go (Avail.AvailTC n ns fs) =
+      let ns' = filter keep ns
+          fs' = filter (keep . flSelector) fs
+      in if null ns' && null fs'
+         then Nothing
+         else Just $ Avail.AvailTC n ns' fs'
+#else
+filterAvails = Avail.filterAvails
+#endif
+
+#if __GLASGOW_HASKELL__ < 802
+bullet :: SDoc
+bullet = unicodeSyntax (char '•') (char '*')
+#endif
+
+
+-- This function was moved and renamed in GHC 8.6
+-- | Check if this kind is Constraint, as seen to the typechecker.
+isConstraintKind :: Kind -> Bool
+#if __GLASGOW_HASKELL__ < 806
+isConstraintKind = Kind.isConstraintKind
+#else
+isConstraintKind = tcIsConstraintKind
+#endif
+
+-- | Similar to `getAnnotations`, but keeps the annotation target.
+--   Also, it is hardcoded to `deserializeWithData`.
+--   Looks only for annotations defined in this module.
+--   Ignores module annotations.
+getModuleAnns :: forall a . Data a => ModGuts -> UniqFM [(Name, a)]
+getModuleAnns = go . mg_anns
+  where
+    valTRep = typeRep (Proxy :: Proxy a)
+    go :: [Annotation] -> UniqFM [(Name, a)]
+    go [] = emptyUFM
+    go (Annotation
+         (NamedTarget n) -- ignore module targets
+         (Serialized trep bytes)
+        : as)
+      | trep == valTRep -- match type representations
+      = addToUFM_Acc (:) (:[]) (go as) n (n, deserializeWithData bytes)
+    -- ignore non-matching annotations
+    go (_:as) = go as
+
+
+
+-- | Similar to Unify.tcMatchTyKis, but looks if there is non-trivial subtype
+--   in the first type that matches the second.
+--   Non-trivial means not a TyVar.
+recMatchTyKi :: Type -> Type -> Maybe TCvSubst
+recMatchTyKi tsearched ttemp = go tsearched
+  where
+    go :: Type -> Maybe TCvSubst
+    go t
+        -- ignore plain TyVars
+      | isTyVarTy t
+        = Nothing
+        -- found a good substitution
+      | Just sub <- matchIt t ttemp
+        = Just sub
+        -- split type constructors
+      | Just (_, tys) <- splitTyConApp_maybe t
+        = getFirst $ foldMap (First . go) tys
+        -- split foralls
+      | (_:_, t') <- splitForAllTys t
+        = go t'
+        -- split arrow types
+      | Just (at, rt) <- splitFunTy_maybe t
+        = go at <|> go rt
+      | otherwise
+        = Nothing
+#if __GLASGOW_HASKELL__ >= 802
+    matchIt = Unify.tcMatchTyKi
+#else
+    matchIt = Unify.tcMatchTy
+#endif
+
+-- | Replace all occurrences of one type in another.
+replaceTypeOccurrences :: Type -> Type -> Type -> Type
+replaceTypeOccurrences told tnew = replace
+  where
+    replace :: Type -> Type
+    replace t
+        -- found occurrence
+      | eqType t told
+        = tnew
+        -- split type constructors
+      | Just (tyCon, tys) <- splitTyConApp_maybe t
+        = mkTyConApp tyCon $ map replace tys
+        -- split foralls
+      | (bndrs@(_:_), t') <- splitForAllTys t
+        = mkSpecForAllTys bndrs $ replace t'
+        -- split arrow types
+      | Just (at, rt) <- splitFunTy_maybe t
+        = mkFunTy (replace at) (replace rt)
+        -- could not find anything
+      | otherwise
+        = t
+
+
+
+-- | Define the behavior for the instance selection.
+--   Mirrors `BasicTypes.OverlapMode`, but does not have a `SourceText` field.
+data OverlapMode
+  = NoOverlap
+    -- ^ This instance must not overlap another `NoOverlap` instance.
+    --   However, it may be overlapped by `Overlapping` instances,
+    --   and it may overlap `Overlappable` instances.
+  | Overlappable
+    -- ^ Silently ignore this instance if you find a
+    --   more specific one that matches the constraint
+    --   you are trying to resolve
+  | Overlapping
+    -- ^ Silently ignore any more general instances that may be
+    --   used to solve the constraint.
+  | Overlaps
+    -- ^ Equivalent to having both `Overlapping` and `Overlappable` flags.
+  | Incoherent
+    -- ^ Behave like Overlappable and Overlapping, and in addition pick
+    --   an an arbitrary one if there are multiple matching candidates, and
+    --   don't worry about later instantiation
+  deriving (Eq, Show, Read, Data)
+
+
+toOverlapFlag :: OverlapMode -> OverlapFlag
+toOverlapFlag m = OverlapFlag (getOMode m) False
+  where
+    getOMode NoOverlap    = GhcPlugins.NoOverlap noSourceText
+    getOMode Overlapping  = GhcPlugins.Overlapping noSourceText
+    getOMode Overlappable = GhcPlugins.Overlappable noSourceText
+    getOMode Overlaps     = GhcPlugins.Overlaps noSourceText
+    getOMode Incoherent   = GhcPlugins.Incoherent noSourceText
+
+#if __GLASGOW_HASKELL__ >= 802
+    noSourceText = GhcPlugins.NoSourceText
+#else
+    noSourceText = "[plugin-generated code]"
+#endif
+
+
+
+
+
+pnConstraintsDeriving :: FastString
+pnConstraintsDeriving = mkFastString "constraints-deriving"
+
+pnConstraints :: FastString
+pnConstraints = mkFastString "constraints"
+
+pnBase :: FastString
+pnBase = mkFastString "base"
+
+mnConstraint :: ModuleName
+mnConstraint = mkModuleName "Data.Constraint"
+
+mnConstraintBare :: ModuleName
+mnConstraintBare = mkModuleName "Data.Constraint.Bare"
+
+mnDeriveAll :: ModuleName
+mnDeriveAll = mkModuleName "Data.Constraint.Deriving.DeriveAll"
+
+mnToInstance :: ModuleName
+mnToInstance = mkModuleName "Data.Constraint.Deriving.ToInstance"
+
+mnDataTypeEquality :: ModuleName
+mnDataTypeEquality = mkModuleName "Data.Type.Equality"
+
+tnDict :: OccName
+tnDict = mkTcOcc "Dict"
+
+tnBareConstraint :: OccName
+tnBareConstraint = mkTcOcc "BareConstraint"
+
+tnDeriveContext :: OccName
+tnDeriveContext = mkTcOcc "DeriveContext"
+
+vnDictToBare :: OccName
+vnDictToBare = mkVarOcc "dictToBare"
+
+cnTypeEq :: OccName
+cnTypeEq = mkTcOcc "~"
+ src/Data/Constraint/Deriving/DeriveAll.hs view
@@ -0,0 +1,906 @@+{-# LANGUAGE CPP                #-}
+{-# LANGUAGE DataKinds          #-}
+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE KindSignatures     #-}
+{-# LANGUAGE LambdaCase         #-}
+{-# LANGUAGE OverloadedStrings  #-}
+{-# LANGUAGE RecordWildCards    #-}
+{-# LANGUAGE TypeFamilies       #-}
+module Data.Constraint.Deriving.DeriveAll
+  ( DeriveAll (..), DeriveContext
+  , deriveAllPass
+  , CorePluginEnvRef, initCorePluginEnv
+  ) where
+
+
+import           Class               (Class, classTyCon)
+import           CoAxiom             (CoAxBranch, coAxBranchIncomps,
+                                      coAxBranchLHS, coAxBranchRHS,
+                                      coAxiomBranches, coAxiomSingleBranch,
+                                      fromBranches)
+import           Control.Applicative (Alternative (..))
+import           Control.Arrow       (second)
+import           Control.Monad       (join, unless)
+import           Data.Data           (Data)
+import           Data.Either         (partitionEithers)
+import qualified Data.Kind           (Constraint, Type)
+import           Data.List           (groupBy, isPrefixOf, sortOn)
+import           Data.Maybe          (catMaybes, fromMaybe)
+import           Data.Monoid         (First (..))
+import qualified FamInstEnv
+import           GhcPlugins          hiding (OverlapMode (..), overlapMode,
+                                      (<>))
+import qualified GhcPlugins
+import           InstEnv             (ClsInst, DFunInstType)
+import qualified InstEnv
+import qualified OccName
+import           Panic               (panicDoc)
+import           TcType              (tcSplitDFunTy)
+import qualified Unify
+
+import Data.Constraint.Deriving.CorePluginM
+
+-- | A marker to tell the core plugin to derive all visible class instances
+--      for a given newtype.
+--
+--   The deriving logic is to simply re-use existing instance dictionaries
+--      by casting them.
+data DeriveAll = DeriveAll
+  deriving (Eq, Show, Read, Data)
+
+
+-- | This type family is used to impose constraints on type parameters when
+--   looking up type instances for the `DeriveAll` core plugin.
+--
+--   `DeriveAll` uses only those instances that satisfy the specified constraint.
+--   If the constraint is not specified, it is assumed to be `()`.
+type family DeriveContext (t :: Data.Kind.Type) :: Data.Kind.Constraint
+
+-- | Run `DeriveAll` plugin pass
+deriveAllPass :: CorePluginEnvRef -> CoreToDo
+deriveAllPass eref = CoreDoPluginPass "Data.Constraint.Deriving.DeriveAll"
+  -- if a plugin pass totally  fails to do anything useful,
+  -- copy original ModGuts as its output, so that next passes can do their jobs.
+  (\x -> fromMaybe x <$> runCorePluginM (deriveAllPass' x) eref)
+
+{-
+  Derive all specific instances of a type for its newtype wrapper.
+
+  Steps:
+
+  1. Lookup a type or type family instances (branches of CoAxiom)
+       of referenced by the newtype decl
+
+  2. For every type instance:
+
+     2.1 Lookup all class instances
+
+     2.2 For every class instance:
+
+         * Use mkLocalInstance with parameters of found instance
+             and replaced RHS types
+         * Create a corresponding top-level binding (DFunId),
+             add it to mg_binds of ModGuts.
+         * Add new instance to (mg_insts :: [ClsInst]) of ModGuts
+         * Update mg_inst_env of ModGuts accordingly.
+
+ -}
+deriveAllPass' :: ModGuts -> CorePluginM ModGuts
+deriveAllPass' gs = go (mg_tcs gs) annotateds gs
+  where
+    annotateds :: UniqFM [(Name, DeriveAll)]
+    annotateds = getModuleAnns gs
+
+    go :: [TyCon] -> UniqFM [(Name, DeriveAll)] -> ModGuts -> CorePluginM ModGuts
+    -- All exports are processed, just return ModGuts
+    go [] anns guts = do
+      unless (isNullUFM anns) $
+        pluginWarning $ "One or more DeriveAll annotations are ignored:"
+          $+$ vcat
+            (map (pprBulletNameLoc . fst) . join $ eltsUFM anns)
+          $+$ "Note, DeriveAll is meant to be used only on type declarations."
+      return guts
+
+    -- process type definitions present in the set of annotations
+    go (x:xs) anns guts
+      | Just ((xn,_):ds) <- lookupUFM anns x = do
+      unless (null ds) $
+        pluginLocatedWarning (nameSrcSpan xn) $
+          "Ignoring redundant DeriveAll annotions" $$
+          hcat
+          [ "(the plugin needs only one annotation per type declaration, but got "
+          , speakN (length ds + 1)
+          , ")"
+          ]
+      pluginDebug $ "DeriveAll invoked on TyCon" <+> ppr x
+      (newInstances, newBinds) <- unzip . fromMaybe [] <$> try (deriveAll x guts)
+      -- add new definitions and continue
+      go xs (delFromUFM anns x) guts
+        { mg_insts    = newInstances ++ mg_insts guts
+        --   I decided to not modify mg_inst_env so that DeriveAll-derived instances
+        --   do not refer to each other.
+        --   Overwise, the result of the plugin would depend on the order of
+        --   type declaration, which would be not good at all.
+        -- , mg_inst_env = InstEnv.extendInstEnvList (mg_inst_env guts) newInstances
+        , mg_binds    = newBinds ++ mg_binds guts
+        }
+
+    -- ignore the rest of type definitions
+    go (_:xs) anns guts = go xs anns guts
+
+    pprBulletNameLoc n = hsep
+      [" ", bullet, ppr $ occName n, ppr $ nameSrcSpan n]
+
+
+
+{- |
+  At this point, the plugin has found a candidate type.
+  The first thing I do here is to make sure this
+    is indeed a proper newtype declaration.
+  Then, lookup the DeriveContext-specified constraints.
+  Then, enumerate specific type instances (based on constraints
+    and type families in the newtype def.)
+  Then, lookup all class instances for the found type instances.
+ -}
+deriveAll :: TyCon -> ModGuts -> CorePluginM [(InstEnv.ClsInst, CoreBind)]
+deriveAll tyCon guts
+-- match good newtypes only
+  | True <- isNewTyCon tyCon
+  , False <- isClassTyCon tyCon
+  , [dataCon] <- tyConDataCons tyCon
+    = do
+      dcInsts <- lookupDeriveContextInstances guts tyCon
+      pluginDebug
+        . hang "DeriveAll (1): DeriveContext instances:" 2
+        . vcat $ map ppr dcInsts
+      unpackedInsts <-
+        if null dcInsts
+        then (:[]) <$> mockInstance tyCon
+        else return $ map unpackInstance dcInsts
+      pluginDebug
+        . hang "DeriveAll (1): DeriveContext instance parameters and RHSs:" 2
+        . vcat $ map ppr unpackedInsts
+      allMatchingTypes <- join <$>
+        traverse (lookupMatchingBaseTypes guts tyCon dataCon) unpackedInsts
+      pluginDebug
+        . hang "DeriveAll (2): matching base types:" 2
+        . vcat $ map ppr allMatchingTypes
+      r <- join <$> traverse (lookupMatchingInstances guts) allMatchingTypes
+      pluginDebug
+        . hang "DeriveAll (3): matching class instances:" 2
+        . vcat $ map (ppr . fst) r
+      return r
+
+-- not a good newtype declaration
+  | otherwise
+    = pluginLocatedError
+       (nameSrcSpan $ tyConName tyCon)
+       "DeriveAll works only on plain newtype declarations"
+
+  where
+    mockInstance tc = do
+      let tvs = tyConTyVars tc
+          tys = mkTyVarTys tvs
+      rhs <- ask tyEmptyConstraint
+      return (tys, rhs)
+    unpackInstance i
+      = let tys  = case tyConAppArgs_maybe <$> FamInstEnv.fi_tys i of
+              [Just ts] -> ts
+              _ -> panicDoc "DeriveAll" $
+                hsep
+                  [ "I faced an impossible type when"
+                      <+> "matching an instance of type family DeriveContext:"
+                  , ppr i, "at"
+                  , ppr $ nameSrcSpan $ getName i]
+            rhs = FamInstEnv.fi_rhs i
+        in (tys, rhs)
+
+
+-- | Find all instance of a type family in scope by its TyCon.
+lookupTyFamInstances :: ModGuts -> TyCon -> CorePluginM [FamInstEnv.FamInst]
+lookupTyFamInstances guts fTyCon = do
+    pkgFamInstEnv <- liftCoreM getPackageFamInstEnv
+    return $ FamInstEnv.lookupFamInstEnvByTyCon
+               (pkgFamInstEnv, mg_fam_inst_env guts) fTyCon
+
+-- | Find all possible instances of DeriveContext type family for a given TyCon
+lookupDeriveContextInstances :: ModGuts -> TyCon -> CorePluginM [FamInstEnv.FamInst]
+lookupDeriveContextInstances guts tyCon = do
+    allInsts <- ask tyConDeriveContext >>= lookupTyFamInstances guts
+    return $ filter check allInsts
+  where
+    check fi = case tyConAppTyCon_maybe <$> FamInstEnv.fi_tys fi of
+      Just tc : _ -> tc == tyCon
+      _           -> False
+
+
+-- | Result of base type lookup, matching, and expanding
+data MatchingType
+  = MatchingType
+  { mtCtxEqs      :: [(TyVar, Type)]
+    -- ^ Current list of constraints that I may want to process
+    --   during type expansion or substitution
+  , mtTheta       :: ThetaType
+    -- ^ Irreducible constraints
+    --      (I can prepend them in the class instance declarations)
+  , mtOverlapMode :: OverlapMode
+    -- ^ How to declare a class instance
+  , mtBaseType    :: Type
+    -- ^ The type behind the newtype wrapper
+  , mtNewType     :: Type
+    -- ^ The newtype with instantiated type arguments
+  , mtIgnoreList  :: [Type]
+    -- ^ A list of type families I have already attempted to expand once
+    --   (e.g. wired-in type families or closed families with no equations
+    --         or something recursive).
+  }
+
+instance Outputable MatchingType where
+  ppr MatchingType {..} = vcat
+    [ "MatchingType"
+    , "{ mtCtxEqs      = " GhcPlugins.<> ppr mtCtxEqs
+    , ", mtTheta       = " GhcPlugins.<> ppr mtTheta
+    , ", mtOverlapMode = " GhcPlugins.<> text (show mtOverlapMode)
+    , ", mtBaseType    = " GhcPlugins.<> ppr mtBaseType
+    , ", mtNewType     = " GhcPlugins.<> ppr mtNewType
+    , ", mtIgnorelist  = " GhcPlugins.<> ppr mtIgnoreList
+    , "}"
+    ]
+
+
+-- | Replace TyVar in all components of a MatchingType
+substMatchingType :: TCvSubst -> MatchingType -> MatchingType
+substMatchingType sub MatchingType {..} = MatchingType
+  { mtCtxEqs      = map (second $ substTyAddInScope sub) mtCtxEqs
+  , mtTheta       = map (substTyAddInScope sub) mtTheta
+  , mtOverlapMode = mtOverlapMode
+  , mtBaseType    = substTyAddInScope sub mtBaseType
+  , mtNewType     = substTyAddInScope sub mtNewType
+  , mtIgnoreList  = map (substTyAddInScope sub) mtIgnoreList
+  }
+
+replaceTyMatchingType :: Type -> Type -> MatchingType -> MatchingType
+replaceTyMatchingType oldt newt MatchingType {..} = MatchingType
+  { mtCtxEqs      = map (second rep) mtCtxEqs
+  , mtTheta       = map rep mtTheta
+  , mtOverlapMode = mtOverlapMode
+  , mtBaseType    = rep mtBaseType
+  , mtNewType     = rep mtNewType
+  , mtIgnoreList  = map rep mtIgnoreList
+  }
+  where
+    rep = replaceTypeOccurrences oldt newt
+
+-- | try to get rid of mtCtxEqs by replacing tyvars
+--       by rhs in all components of the MatchingType
+cleanupMatchingType :: MatchingType -> MatchingType
+cleanupMatchingType mt0 = go (groupLists $ mtCtxEqs mt0) mt0 { mtCtxEqs = []}
+  where
+    groupOn f = groupBy (\x y -> f x == f y)
+    flattenSnd []                 = []
+    flattenSnd ([]:xs)            = flattenSnd xs
+    flattenSnd (ts@((tv,_):_):xs) = (tv, map snd ts): flattenSnd xs
+    groupLists = flattenSnd . groupOn fst . sortOn fst
+
+
+    go :: [(TyVar, [Type])] -> MatchingType -> MatchingType
+    go [] mt = mt
+    go ((_, []):xs) mt = go xs mt
+    -- TyVar occurs once in mtCtxEqs: I can safely replace it in the type.
+    go ((tv,[ty]):xs) mt
+      = let sub = extendTCvSubst emptyTCvSubst tv ty
+        in go (map (second (map $ substTyAddInScope sub)) xs)
+              $ substMatchingType sub mt
+    -- TyVar occurs more than once: it may indicate
+    --       a trivial substition or contradiction
+    go ((tv, tys):xs) mt
+      = case removeEqualTypes tys of
+          []  -> go xs mt -- redundant, but compiler is happy
+          [t] -> go ((tv, [t]):xs) mt
+          ts  -> go xs mt { mtCtxEqs = mtCtxEqs mt ++ map ((,) tv) ts }
+
+    removeEqualTypes [] = []
+    removeEqualTypes [t] = [t]
+    removeEqualTypes (t:ts)
+      | any (eqType t) ts = removeEqualTypes ts
+      | otherwise         = t : removeEqualTypes ts
+
+
+-- | Try to strip trailing TyVars from the base and newtypes,
+--   thus matching higher-kinded types.
+--   This way I can also derive things like Monad & co
+tryHigherRanks :: MatchingType -> [MatchingType]
+tryHigherRanks mt@MatchingType {..}
+  | Just (mtBaseType', bt) <- splitAppTy_maybe mtBaseType
+  , Just (mtNewType' , nt) <- splitAppTy_maybe mtNewType
+  , Just btv <- getTyVar_maybe bt
+  , Just ntv <- getTyVar_maybe nt
+  , btv == ntv
+    -- No constraints or anything else involving our TyVar
+  , not . elem btv
+        . (map fst mtCtxEqs ++)
+        . tyCoVarsOfTypesWellScoped
+      $ [mtBaseType', mtNewType']
+        ++ map snd mtCtxEqs
+        ++ mtTheta
+        ++ mtIgnoreList
+  = let mt' = mt
+          { mtBaseType = mtBaseType'
+          , mtNewType  = mtNewType'
+          }
+    in mt : tryHigherRanks mt'
+tryHigherRanks mt = [mt]
+
+-- | For a given type and constraints, enumerate all possible concrete types;
+--   specify overlapping mode if encountered with conflicting instances of
+--   closed type families.
+--
+lookupMatchingBaseTypes :: ModGuts
+                        -> TyCon
+                        -> DataCon
+                        -> ([Type], Type)
+                        -> CorePluginM [MatchingType]
+lookupMatchingBaseTypes guts tyCon dataCon (tys, constraints) = do
+    ftheta <- filterTheta theta
+    let initMt = MatchingType
+          { mtCtxEqs      = fst ftheta
+          , mtTheta       = snd ftheta
+          , mtOverlapMode = NoOverlap
+          , mtBaseType    = baseType
+          , mtNewType     = newType
+          , mtIgnoreList  = []
+          }
+    (>>= tryHigherRanks . cleanupMatchingType)
+         . take 1000 -- TODO: improve the logic and the termination rule
+        <$> go (cleanupMatchingType initMt)
+  where
+    go :: MatchingType -> CorePluginM [MatchingType]
+    go mt = expandOneFamily guts mt >>= \case
+      Nothing  -> pure [mt]
+      Just mts -> join <$> traverse go mts
+
+    newType = mkTyConApp tyCon tys
+              -- mkFunTys theta $ mkTyConApp tyCon tys
+    theta = splitCts constraints ++ dataConstraints
+
+    splitCts c = case splitTyConApp_maybe c of
+      Nothing       -> [c]
+      Just (tc, ts) ->
+        if isCTupleTyConName $ getName tc
+        then foldMap splitCts ts
+        else [c]
+
+    (dataConstraints, baseType) = case dataConInstSig dataCon tys of
+      ([], cts, [bt]) -> (cts, bt)
+      _ -> panicDoc "DeriveAll" $ hsep
+        [ "Impossible happened:"
+        , "expected a newtype constructor"
+        , "with no existential tyvars and a single type argument,"
+        , "but got", ppr dataCon
+        , "at", ppr $ nameSrcSpan $ getName dataCon ]
+
+{-
+  New plan for generating matching types
+
+
+  Split ThetaType into two lists:
+
+  [(TyVar, Type)] and the rest of ThetaType
+
+  The rest of ThetaType is considered not useful;
+  it will be just appended to a list of constraints in the result types.
+  [(TyVar, Type)] is a list of equality constraints that might help the algorithm.
+
+  I want to perform three operations related to this list:
+  [1] Add new tyVar ~ TypeFamily, from type family occurrences
+       in the base or newtypes
+      (but also check this type family is not present in the eqs?)
+  [2] Remove an item (TypeFamily) from the list by substituting
+        all possible type family instances
+      into the the base type, the newtype, and the list of constraints.
+  [3] Remove a non-TypeFamily item (i.e. a proper data/newtype TyCon)
+      by substituting TyVar with
+      this type in the base type, the newtype, and the list of constraints.
+
+  Actions [1,2] may lead to an infinite expansion (recursive families)
+  so I need to bound the number of iterations. An approximate implementation plan:
+  1. Apply [1] until no type families present in the basetype or the newtype
+  2. Apply [2] or [3] until no esq left???
+
+ -}
+
+
+-- | Split constraints into two groups:
+--   1. The ones used as substitutions
+--   2. Irreducible ones w.r.t. the type expansion algorithm
+filterTheta :: ThetaType -> CorePluginM ([(TyVar, Type)], ThetaType)
+filterTheta = fmap (partitionEithers . join) . traverse
+  (\t -> do
+    teqClass <- ask classTypeEq
+    filterTheta' teqClass t
+  )
+
+-- "worker" part of filterTheta (with a provided reference to "~")
+filterTheta' :: Class -> Type -> CorePluginM [Either (TyVar, Type) PredType]
+filterTheta' teqClass t = go (classifyPredType t)
+  where
+    go (EqPred _ t1 t2)
+      | Just tv <- getTyVar_maybe t1
+        = return [Left (tv, t2)]
+      | Just tv <- getTyVar_maybe t2
+        = return [Left (tv, t1)]
+      | otherwise
+        = do
+        tv <- newTyVar (typeKind t1)
+        return [Left (tv, t1), Left (tv, t2)]
+    go (ClassPred c ts)
+      | c == heqClass
+      , [_, _, t1, t2] <- ts
+          -- nominal or rep-al equality does not matter here, because
+          -- I don't distinguish between those a few lines above.
+        = go (EqPred ReprEq t1 t2)
+      | c == teqClass
+      , [_, t1, t2] <- ts
+        = go (EqPred ReprEq t1 t2)
+      | otherwise
+        = return [Right t]
+    go _ = return [Right t]
+
+expandOneFamily :: ModGuts -> MatchingType -> CorePluginM (Maybe [MatchingType])
+expandOneFamily guts mt@MatchingType{..} = case mfam of
+    Nothing      -> return Nothing
+    Just (ff, t) -> expandFamily guts ff t >>= \case
+        Nothing -> return $ Just [mt { mtIgnoreList = t : mtIgnoreList }]
+        Just es -> return $ Just $ map (toMT t) es
+  where
+    -- first, substitute all type variables,
+    -- then substitute family occurrence with RHS of the axiom (rezt)
+    toMT ft (omode, rezt, subst)
+      = let famOcc = substTyAddInScope subst ft
+            newMt  = substMatchingType subst mt
+        in if eqType ft rezt
+           then mt { mtIgnoreList = ft : mtIgnoreList }
+           else replaceTyMatchingType famOcc rezt newMt
+                  { mtOverlapMode = omode }
+
+
+    -- Lookup through all components
+    look = First . lookupFamily mtIgnoreList
+    First mfam = mconcat
+      [ foldMap (look . snd) mtCtxEqs
+      , foldMap look mtTheta
+      , look mtBaseType
+      , look mtNewType
+      ]
+
+
+-- -- TODO: Not sure if I need it at all;
+--                   most of the API functions look through synonyms
+-- -- | Try to remove all occurrences of type synonyms.
+-- clearSynonyms :: Type -> Type
+-- clearSynonyms t'
+--       -- split type constructors
+--     | Just (tyCon, tys) <- splitTyConApp_maybe t
+--       = mkTyConApp tyCon $ map clearSynonyms tys
+--       -- split foralls
+--     | (bndrs@(_:_), t1) <- splitForAllTys t
+--       = mkSpecForAllTys bndrs $ clearSynonyms t1
+--       -- split arrow types
+--     | Just (at, rt) <- splitFunTy_maybe t
+--       = mkFunTy (clearSynonyms at) (clearSynonyms rt)
+--     | otherwise
+--       = t
+--   where
+--     stripOuter x = case tcView x of
+--       Nothing -> x
+--       Just y  -> stripOuter y
+--     t = stripOuter t'
+
+
+-- | Depth-first lookup of the first occurrence of any type family.
+--   First argument is a list of types to ignore.
+lookupFamily :: [Type] -> Type -> Maybe (FamTyConFlav, Type)
+lookupFamily ignoreLst t
+      -- split type constructors
+    | Just (tyCon, tys) <- splitTyConApp_maybe t
+      = case foldMap (First . lookupFamily ignoreLst) tys of
+          First (Just r) -> Just r
+          First Nothing  -> famTyConFlav_maybe tyCon >>= \ff ->
+            if any (eqType t) ignoreLst
+            then Nothing
+            else Just (ff, t)
+      -- split foralls
+    | (_:_, t') <- splitForAllTys t
+      = lookupFamily ignoreLst t'
+      -- split arrow types
+    | Just (at, rt) <- splitFunTy_maybe t
+      = lookupFamily ignoreLst at <|> lookupFamily ignoreLst rt
+    | otherwise
+      = Nothing
+
+
+-- | Enumerate available family instances and substitute type arguments,
+--   such that original type family can be replaced with any
+--     of the types in the output list.
+--   It passes a TCvSubst alongside with the substituted Type.
+--   The substituted Type may have TyVars from the result set of the substitution,
+--   thus I must be careful with using it:
+--     either somehow substitute back these tyvars from the result,
+--     or substitute the whole type that contains this family occurrence.
+--
+--   return Nothing   means cannot expand family (shall use it as-is);
+--   return (Just []) means all instances contradict family arguments.
+expandFamily :: ModGuts
+             -> FamTyConFlav
+             -> Type
+             -> CorePluginM (Maybe [(OverlapMode, Type, TCvSubst)])
+-- cannot help here
+expandFamily _ AbstractClosedSynFamilyTyCon{} _ = pure Nothing
+-- .. and here
+expandFamily _ BuiltInSynFamTyCon{}           _ = pure Nothing
+-- .. closed type families with no equations cannot be helped either
+expandFamily _ (ClosedSynFamilyTyCon Nothing) _ = pure Nothing
+-- For a closed type family, equations are accessible right there
+expandFamily _ (ClosedSynFamilyTyCon (Just coax)) ft
+    = withFamily ft (pure Nothing) $ const $ expandClosedFamily os bcs
+  where
+    bcs = fromBranches $ coAxiomBranches coax
+    os  = if any (not . null . coAxBranchIncomps) bcs
+          then map overlap bcs else repeat NoOverlap
+    overlap cb = if null $ coAxBranchIncomps cb
+          then Overlapping
+          else Incoherent
+-- For a data family or an open type family, I need to lookup instances
+-- in the family instance environment.
+expandFamily guts DataFamilyTyCon{} ft
+  = withFamily ft (pure Nothing) $ expandDataFamily guts
+expandFamily guts OpenSynFamilyTyCon ft
+  = withFamily ft (pure Nothing) $ expandOpenFamily guts
+
+withFamily :: Type -> a -> (TyCon -> [Type] -> a) -> a
+withFamily ft def f = case splitTyConApp_maybe ft of
+  Nothing       -> def
+  Just (tc, ts) -> f tc ts
+
+
+-- | The same as `expandFamily`, but I know already that the family is closed.
+expandClosedFamily :: [OverlapMode]
+                   -> [CoAxBranch]
+                   -> [Type] -> CorePluginM (Maybe [(OverlapMode, Type, TCvSubst)])
+-- empty type family -- leave it as-is
+expandClosedFamily _ [] _ = pure Nothing
+expandClosedFamily os bs fTyArgs = fmap (Just . catMaybes) $ traverse go $ zip os bs
+  where
+    go (om, cb) = do
+      let flhs' = coAxBranchLHS cb
+          n = length flhs'
+          tvs' = tyCoVarsOfTypesWellScoped flhs'
+      tvs <- traverse freshenTyVar tvs'
+      let freshenSub = zipTvSubst tvs' $ map mkTyVarTy tvs
+          flhs = substTys freshenSub flhs'
+          frhs = substTyAddInScope freshenSub $ coAxBranchRHS cb
+          t = foldl mkAppTy frhs $ drop n fTyArgs
+          msub = Unify.tcMatchTys (take n fTyArgs) flhs
+      return $ (,,) om t <$> msub
+
+
+
+-- | The same as `expandFamily`, but I know already that the family is open.
+expandOpenFamily :: ModGuts
+                 -> TyCon  -- ^ Type family construtor
+                 -> [Type] -- ^ Type family arguments
+                 -> CorePluginM (Maybe [(OverlapMode, Type, TCvSubst)])
+expandOpenFamily guts fTyCon fTyArgs = do
+  tfInsts <- lookupTyFamInstances guts fTyCon
+  if null tfInsts
+    then pure $ Just [] -- No mercy
+    else expandClosedFamily
+           (repeat NoOverlap)
+           (coAxiomSingleBranch . FamInstEnv.famInstAxiom <$> tfInsts)
+           fTyArgs
+
+
+-- | The same as `expandFamily`, but I know already that this is a data family.
+expandDataFamily :: ModGuts
+                 -> TyCon  -- ^ Type family construtor
+                 -> [Type] -- ^ Type family arguments
+                 -> CorePluginM (Maybe [(OverlapMode, Type, TCvSubst)])
+expandDataFamily guts fTyCon fTyArgs = do
+  tfInsts <- lookupTyFamInstances guts fTyCon
+  if null tfInsts
+    then pure $ Just [] -- No mercy
+    else sequence <$> traverse expandDInstance tfInsts
+  where
+    expandDInstance inst
+      | fitvs <- FamInstEnv.fi_tvs inst
+      = do
+      tvs <- traverse freshenTyVar $ fitvs
+      let freshenSub = zipTvSubst fitvs $ map mkTyVarTy tvs
+          fitys = substTys freshenSub $ FamInstEnv.fi_tys inst
+          instTyArgs = align fTyArgs fitys
+      return $ (,,) NoOverlap (mkTyConApp fTyCon instTyArgs)
+        <$> Unify.tcMatchTys fTyArgs instTyArgs
+    align [] _          = []
+    align xs []         = xs
+    align (_:xs) (y:ys) = y : align xs ys
+
+
+data MatchingInstance = MatchingInstance
+  { miInst       :: ClsInst
+    -- ^ Original found instance for the base type (as declared somewhere);
+    --   It contains the signature and original DFunId
+  , miInstTyVars :: [DFunInstType]
+    -- ^ How TyVars of miOrigBaseClsInst should be replaced to make it as
+    --   an instance for the base type;
+    --   e.g. a TyVar may be instantiated with a concrete type
+    --         (which may or may not contain more type variables).
+  , miTheta      :: [(PredType, MatchingPredType)]
+    -- ^ Original pred types and how they are going to be transformed
+  }
+
+instance Outputable MatchingInstance where
+  ppr MatchingInstance {..} = hang "MatchingInstance" 2 $ vcat
+    [ "{ miInst       =" <+> ppr miInst
+    , ", miInstTyVars =" <+> ppr miInstTyVars
+    , ", miTheta      =" <+> ppr miTheta
+    ]
+
+{-
+Resolving theta types:
+
+1. Class constraints: every time check
+   a. if there is an instance, substitute corresponding DFunIds and be happy.
+   b. if there is no instance and no tyvars, then fail
+   c. otherwise propagate the constraint further.
+
+2. Equality constraints: check equality
+   a. Types are equal (and tyvars inside equal as well):
+      Substitute mkReflCo
+   b. Types are unifiable:
+      Propagate constraint further
+   c. Types are non-unifiable:
+      Discard the whole instance declaration.
+ -}
+data MatchingPredType
+  = MptInstance MatchingInstance
+    -- ^ Found an instance
+  | MptReflexive Coercion
+    -- ^ The equality become reflexive after a tyvar substitution
+  | MptPropagateAs PredType
+    -- ^ Could do nothing, but there is still hope due to the present tyvars
+
+instance Outputable MatchingPredType where
+  ppr (MptInstance x)    = "MptInstance" <+> ppr x
+  ppr (MptReflexive x)   = "MptReflexive" <+> ppr x
+  ppr (MptPropagateAs x) = "MptPropagateAs" <+> ppr x
+
+findInstance :: InstEnv.InstEnvs
+             -> Type
+             -> ClsInst
+             -> Maybe MatchingInstance
+findInstance ie t i
+  | -- Most important: some part of the instance parameters must unify to arg
+    Just sub <- getFirst $ foldMap (First . flip recMatchTyKi t) iTyPams
+    -- substituted type parameters of the class
+  , newTyPams <- map (substTyAddInScope sub) iTyPams
+    -- This tells us how instance tyvars change after matching the type
+    = matchInstance ie iClass newTyPams
+  | otherwise
+    = Nothing
+  where
+    (_, _, iClass, iTyPams) = InstEnv.instanceSig i
+
+
+matchInstance :: InstEnv.InstEnvs
+              -> Class
+              -> [Type]
+              -> Maybe MatchingInstance
+matchInstance ie cls ts
+  | ([(i, tyVarSubs)], _notMatchButUnify, _safeHaskellStuff)
+      <- InstEnv.lookupInstEnv False ie cls ts
+  , (iTyVars, iTheta, _, _) <- InstEnv.instanceSig i
+  , sub <- mkTvSubstPrs
+         . catMaybes $ zipWith (fmap . (,)) iTyVars tyVarSubs
+    = do
+
+    mpts <- traverse (matchPredType ie . substTyAddInScope sub) iTheta
+    return MatchingInstance
+      { miInst = i
+      , miInstTyVars = tyVarSubs
+      , miTheta = zip iTheta mpts
+      }
+  | otherwise
+    = Nothing
+
+matchPredType :: InstEnv.InstEnvs
+              -> PredType
+              -> Maybe MatchingPredType
+matchPredType ie pt = go $ classifyPredType pt
+  where
+    go (ClassPred cls ts)
+      | Just mi <- matchInstance ie cls ts
+                       = Just $ MptInstance mi
+        -- we could not find an instance, but also there are no tyvars (and no hope)
+      | [] <- tyCoVarsOfTypesWellScoped ts
+                       = Nothing
+      | otherwise      = Just $ MptPropagateAs pt
+    go (EqPred rel t1 t2)
+      | eqType t1 t2   = Just . MptReflexive $ case rel of
+                                          NomEq  -> mkReflCo Nominal t1
+                                          ReprEq -> mkReflCo Representational t1
+      | Unify.typesCantMatch [(t1,t2)]
+                       = Nothing
+      | otherwise      = Just $ MptPropagateAs pt
+    go _               = Just $ MptPropagateAs pt
+
+
+type TyExp = (Type, CoreExpr)
+type TyBndr = (Type, CoreBndr)
+
+
+mtmiToExpression :: MatchingType
+                 -> MatchingInstance
+                 -> CorePluginM TyExp
+mtmiToExpression MatchingType {..} mi = do
+  (bndrs, (tOrig, e)) <- miToExpression' [] mi
+  let extraTheta
+            = filter (\t -> not $ any (eqType t . fst) bndrs) mtTheta
+      tRepl = replaceTypeOccurrences mtBaseType mtNewType tOrig
+      tFun  = mkFunTys (extraTheta ++ map fst bndrs) tRepl
+      tvs   = tyCoVarsOfTypeWellScoped tFun
+  return
+    ( mkSpecForAllTys tvs tFun
+    , mkCoreLams (tvs ++ map mkWildValBinder extraTheta ++ map snd bndrs)
+      $ mkCast e
+      $ mkUnsafeCo Representational tOrig tRepl
+    )
+
+
+-- | Construct a core expression and a corresponding type.
+--   It does not bind arguments;
+--   uses only types and vars present in MatchinInstance;
+--   may create a few vars for PredTypes, they are returned in fst.
+miToExpression' :: [TyExp]
+                   -- ^ types and expressions of the PredTypes that are in scope
+                -> MatchingInstance
+                -> CorePluginM ([TyBndr], TyExp)
+                   -- (what to add to lambda, and the final expression)
+miToExpression' availPTs MatchingInstance {..} = do
+    (bndrs, eArgs) <- addArgs availPTs $ map snd miTheta
+    return
+      ( bndrs
+      , ( newIHead
+        , mkCoreApps eDFunWithTyPams eArgs
+        )
+      )
+  where
+    (iTyVars, _, iClass, iTyPams) = InstEnv.instanceSig miInst
+    -- this is the same length as iTyVars, needs to be applied on dFunId
+    tyVarVals = zipWith (fromMaybe . mkTyVarTy) iTyVars miInstTyVars
+    sub = mkTvSubstPrs . catMaybes
+          $ zipWith (fmap . (,)) iTyVars miInstTyVars
+    newTyPams = map (substTyAddInScope sub) iTyPams
+    newIHead = mkTyConApp (classTyCon iClass) newTyPams
+    eDFun = Var $ InstEnv.instanceDFunId miInst
+    eDFunWithTyPams = mkTyApps eDFun tyVarVals
+    addArgs :: [TyExp]
+            -> [MatchingPredType]
+            -> CorePluginM ([TyBndr], [CoreExpr])
+    addArgs _   []    = pure ([], [])
+    addArgs ps (x:xs) = do
+      (tbdrs, e) <- mptToExpression ps x
+      let ps' = ps ++ map (Var <$>) tbdrs
+      (tbdrs', es) <- addArgs ps' xs
+      return
+        ( tbdrs ++ tbdrs'
+        , e:es
+        )
+
+
+-- | Construct an expression to put as a PredType argument.
+--   It may need to produce a new type variable.
+mptToExpression :: [TyExp]
+                -> MatchingPredType
+                -> CorePluginM ([TyBndr], CoreExpr)
+mptToExpression ps (MptInstance mi)
+  = fmap snd <$> miToExpression' ps mi
+mptToExpression _  (MptReflexive c)
+  = pure ([], Coercion c)
+mptToExpression ps (MptPropagateAs pt)
+  = case mte of
+    Just e -> pure ([], e)
+    Nothing -> do
+      loc <- liftCoreM getSrcSpanM
+      u <- getUniqueM
+      let n = mkInternalName u
+                (mkOccName OccName.varName $ "dFunArg_" ++ show u) loc
+          v = mkLocalIdOrCoVar n pt
+      return ([(pt,v)], Var v)
+  where
+      mte = getFirst $ foldMap getSamePT ps
+      getSamePT (t, e)
+        | eqType t pt = First $ Just e
+        | otherwise    = First Nothing
+
+-- | For a given most concrete type, find all possible class instances.
+--   Derive them all by creating a new CoreBind with a casted type.
+--
+--   Prerequisite: in the tripple (overlapmode, baseType, newType),
+--   TyVars of the newType must be a superset of TyVars of the baseType.
+lookupMatchingInstances :: ModGuts
+                        -> MatchingType
+                        -> CorePluginM [(ClsInst, CoreBind)]
+lookupMatchingInstances guts mt
+    | Just bTyCon <- tyConAppTyCon_maybe $ mtBaseType mt = do
+      ie <- getInstEnvs guts
+      let clsInsts = lookupClsInsts ie bTyCon
+      pluginDebug $ hang "lookupMatchingInstances candidate instances:" 2 $
+        vcat $ map ppr clsInsts
+      catMaybes <$> traverse (lookupMatchingInstance ie mt) clsInsts
+    | otherwise = fmap (const []) . pluginDebug $ hcat
+        [ text "DeriveAll.lookupMatchingInstances found no class instances for "
+        , ppr (mtBaseType mt)
+        , text ", because it could not get the type constructor."
+        ]
+
+
+lookupMatchingInstance :: InstEnv.InstEnvs
+                       -> MatchingType
+                       -> ClsInst
+                       -> CorePluginM (Maybe (ClsInst, CoreBind))
+lookupMatchingInstance ie mt@MatchingType {..} baseInst
+  | not . unwantedName $ getName iClass
+  , all (noneTy unwantedName) iTyPams
+  , Just mi <- findInstance ie mtBaseType baseInst
+    = do
+    (t, e) <- mtmiToExpression mt mi
+    newN <- newName (occNameSpace baseDFunName)
+      $ occNameString baseDFunName
+        ++ show (getUnique baseDFunId) -- unique per baseDFunId
+        ++ newtypeNameS                -- unique per newType
+    let (newTyVars, _, _, newTyPams) = tcSplitDFunTy t
+        newDFunId = mkExportedLocalId
+          (DFunId isNewType) newN t
+    return $ Just
+      ( InstEnv.mkLocalInstance
+                    newDFunId
+                    (toOverlapFlag mtOverlapMode)
+                    newTyVars iClass newTyPams
+      , NonRec newDFunId e
+      )
+  | otherwise
+    = do
+    pluginDebug $ hang "Ignored instance" 2
+      $ ppr mtBaseType <+> ppr baseInst
+    pure Nothing
+  where
+    baseDFunId = InstEnv.instanceDFunId baseInst
+    (_, _, iClass, iTyPams) = InstEnv.instanceSig baseInst
+    isNewType = isNewTyCon (classTyCon iClass)
+    baseDFunName = occName . idName $ baseDFunId
+    newtypeNameS = case tyConAppTyCon_maybe mtNewType of
+      Nothing -> "DeriveAll-generated"
+      Just tc -> occNameString $ occName $ tyConName tc
+
+
+
+-- checks if none of the names in the type satisfy the predicate
+noneTy :: (Name -> Bool) -> Type -> Bool
+noneTy f = not . uniqSetAny f . orphNamesOfType
+#if __GLASGOW_HASKELL__ < 802
+  where
+    uniqSetAny g = foldl (\a -> (||) a . g) False
+#endif
+
+unwantedName :: Name -> Bool
+unwantedName n
+  | modName == "GHC.Generics"  = True
+  | modName == "Data.Typeable" = True
+  | modName == "Data.Data"     = True
+  | "Language.Haskell.TH"
+          `isPrefixOf` modName = True
+  | valName == "Coercible"     = True
+  | otherwise                  = False
+  where
+    modName = moduleNameString . moduleName $ nameModule n
+    valName = occNameString $ getOccName n
+ src/Data/Constraint/Deriving/ToInstance.hs view
@@ -0,0 +1,262 @@+{-# LANGUAGE DeriveDataTypeable #-}
+{-# LANGUAGE LambdaCase         #-}
+{-# LANGUAGE OverloadedStrings  #-}
+module Data.Constraint.Deriving.ToInstance
+  ( ToInstance (..)
+  , OverlapMode (..)
+  , toInstancePass
+  , CorePluginEnvRef, initCorePluginEnv
+  ) where
+
+import           Class               (Class, classTyCon)
+import           Control.Applicative (Alternative (..))
+import           Control.Monad       (join, unless)
+import           Data.Data           (Data)
+import           Data.Maybe          (fromMaybe, isJust)
+import           Data.Monoid         (First (..))
+import           GhcPlugins          hiding (OverlapMode (..), overlapMode)
+import qualified InstEnv
+import qualified OccName
+import           Panic               (panicDoc)
+import qualified Unify
+
+import Data.Constraint.Deriving.CorePluginM
+
+
+{- | A marker to tell the core plugin to convert a top-level `Data.Constraint.Dict` binding into
+     an instance declaration.
+
+     Example:
+
+@
+type family FooFam a where
+  FooFam Int = Int
+  FooFam a   = Double
+
+data FooSing a where
+  FooInt   :: FooSing Int
+  FooNoInt :: FooSing a
+
+class FooClass a where
+  fooSing :: FooSing a
+
+newtype Bar a = Bar (FooFam a)
+
+{\-\# ANN fooNum (ToInstance NoOverlap) \#-\}
+fooNum :: forall a . Dict (Num (Bar a))
+fooNum = mapDict (unsafeDerive Bar) $ case fooSing @a of
+  FooInt   -> Dict
+  FooNoInt -> Dict
+@
+
+     Note:
+
+     * `fooNum` should be exported by the module
+        (otherwise, it may be optimized-out before the core plugin pass);
+     * Constraints of the function become constraints of the new instance;
+     * The argument of `Dict` must be a single class (no constraint tuples or equality constraints);
+     * The instance is created in a core-to-core pass, so it does not exist for the type checker in the current module.
+ -}
+newtype ToInstance = ToInstance { overlapMode :: OverlapMode }
+  deriving (Eq, Show, Read, Data)
+
+-- | Run `ToInstance` plugin pass
+toInstancePass :: CorePluginEnvRef -> CoreToDo
+toInstancePass eref = CoreDoPluginPass "Data.Constraint.Deriving.ToInstance"
+  -- if a plugin pass totally  fails to do anything useful,
+  -- copy original ModGuts as its output, so that next passes can do their jobs.
+  (\x -> fromMaybe x <$> runCorePluginM (toInstancePass' x) eref)
+
+toInstancePass' :: ModGuts -> CorePluginM ModGuts
+toInstancePass' gs = go (reverse $ mg_binds gs) annotateds gs { mg_binds = []}
+  where
+    annotateds :: UniqFM [(Name, ToInstance)]
+    annotateds = getModuleAnns gs
+
+    go :: [CoreBind] -> UniqFM [(Name, ToInstance)] -> ModGuts -> CorePluginM ModGuts
+    -- All exports are processed, just return ModGuts
+    go [] anns guts = do
+      unless (isNullUFM anns) $
+        pluginWarning $ "One or more ToInstance annotations are ignored:"
+          $+$ vcat
+            (map (pprBulletNameLoc . fst) . join $ eltsUFM anns)
+          $$ "Note possible issues:"
+          $$ pprNotes
+           [ "ToInstance is meant to be used only on bindings of type Ctx => Dict (Class t1 .. tn)."
+           , "Currently, I process non-recursive bindings only."
+           , sep
+             [ "Non-exported bindings may vanish before the plugin pass:"
+             , "make sure you export annotated definitions!"
+             ]
+           ]
+      return guts
+
+    -- process type definitions present in the set of annotations
+    go (cbx@(NonRec x _):xs) anns guts
+      | Just ((xn, ti):ds) <- lookupUFM anns x = do
+      unless (null ds) $
+        pluginLocatedWarning (nameSrcSpan xn) $
+          "Ignoring redundant ToInstance annotions" $$
+          hcat
+          [ "(the plugin needs only one annotation per binding, but got "
+          , speakN (length ds + 1)
+          , ")"
+          ]
+      -- add new definitions and continue
+      try (toInstance ti cbx) >>= \case
+        Nothing
+          -> go xs (delFromUFM anns x) guts { mg_binds = cbx : mg_binds guts}
+        Just (newInstance, newBind)
+          -> go xs (delFromUFM anns x) guts
+            { mg_insts    = newInstance : mg_insts guts
+            , mg_inst_env = InstEnv.extendInstEnv (mg_inst_env guts) newInstance
+            , mg_binds    = cbx : newBind : mg_binds guts
+              -- Remove original binding from the export list
+              --                                if it was there.
+            , mg_exports  = filterAvails (xn /=) $ mg_exports guts
+            }
+
+    -- ignore the rest of bindings
+    go (x:xs) anns guts = go xs anns guts { mg_binds = x : mg_binds guts}
+
+    pprBulletNameLoc n = hsep
+      [" " , bullet, ppr $ occName n, ppr $ nameSrcSpan n]
+    pprNotes = vcat . map (\x -> hsep [" ", bullet, x])
+
+-- | Transform a given CoreBind into an instance.
+--
+--   The input core bind must have type `Ctx => Dict (Class t1 .. tn)`
+--
+--   The output is `instance {-# overlapMode #-} Ctx => Class t1 ... tn`
+toInstance :: ToInstance -> CoreBind -> CorePluginM (InstEnv.ClsInst, CoreBind)
+
+toInstance _ (Rec xs) = do
+    loc <- liftCoreM getSrcSpanM
+    pluginLocatedError
+        (fromMaybe loc $ getFirst $ foldMap (First . Just . nameSrcSpan . getName . fst) xs)
+      $ "ToInstance plugin pass does not support recursive bindings"
+      $$ hsep ["(group:", pprQuotedList (map (getName . fst) xs), ")"]
+
+toInstance (ToInstance omode) (NonRec bindVar bindExpr) = do
+    -- check if all type arguments are constraint arguments
+    unless (all (isConstraintKind . typeKind) theta) $
+      pluginLocatedError loc notGoodMsg
+
+    -- get necessary definitions
+    tcBareConstraint <- ask tyConBareConstraint
+    tcDict <- ask tyConDict
+    fDictToBare <- ask funDictToBare
+    varCls <- newTyVar constraintKind
+    let tyMatcher = mkTyConApp tcDict [mkTyVarTy varCls]
+
+    -- Get instance definition
+    match <- case Unify.tcMatchTy tyMatcher dictTy of
+      Nothing -> pluginLocatedError loc notGoodMsg
+      Just ma -> pure ma
+    let matchedTy = substTyVar match varCls
+        instSig = mkSpecForAllTys bndrs $ mkFunTys theta matchedTy
+        bindBareTy = mkSpecForAllTys bndrs $ mkFunTys theta $ mkTyConApp tcBareConstraint [matchedTy]
+
+    -- check if constraint is indeed a class and get it
+    matchedClass <- case tyConAppTyCon_maybe matchedTy >>= tyConClass_maybe of
+      Nothing -> pluginLocatedError loc notGoodMsg
+      Just cl -> pure cl
+
+    -- try to apply dictToBare to the expression of the found binding
+    newExpr <- case unwrapDictExpr dictTy fDictToBare bindExpr of
+      Nothing -> pluginLocatedError loc notGoodMsg
+      Just ex -> pure $ mkCast ex
+                      $ mkUnsafeCo Representational bindBareTy instSig
+
+
+    mkNewInstance omode matchedClass bindVar newExpr
+
+  where
+    origBindTy = idType bindVar
+    (bndrs, bindTy) = splitForAllTys origBindTy
+    (theta, dictTy) = splitFunTys bindTy
+    loc = nameSrcSpan $ getName bindVar
+    notGoodMsg =
+         "ToInstance plugin pass failed to process a Dict declaraion."
+      $$ "The declaration must have form `forall a1..an . Ctx => Dict (Cls t1..tn)'"
+      $$ "Declaration:"
+      $$ hcat
+         [ "  "
+         , ppr bindVar, " :: "
+         , ppr origBindTy
+         ]
+      $$ ""
+      $$ "Please check:"
+      $$ vcat
+       ( map (\s -> hsep  [" ", bullet, s])
+         [ "It must not have arguments (i.e. is it not a fuction, but a value);"
+         , "It must have type Dict;"
+         , "The argument of Dict must be a single class (e.g. no constraint tuples or equalities);"
+         , "It must not have implicit arguments or any other complicated things."
+         ]
+       )
+
+-- This fails if the CoreExpr type is not valid instance signature.
+mkNewInstance :: OverlapMode
+              -> Class
+              -> Id -- ^ Original core binding (with old type)
+              -> CoreExpr -- ^ implementation, with a proper new type (instance signature)
+              -> CorePluginM (InstEnv.ClsInst, CoreBind)
+mkNewInstance omode cls bindVar bindExpr = do
+    n <- newName OccName.varName
+       $ getOccString bindVar ++ "_ToInstance"
+    let iDFunId = mkExportedLocalId
+          (DFunId $ isNewTyCon (classTyCon cls))
+          n itype
+    return
+      ( InstEnv.mkLocalInstance iDFunId ioflag tvs cls tys
+      , NonRec iDFunId bindExpr
+      )
+  where
+    ioflag  = toOverlapFlag omode
+    itype   = exprType bindExpr
+
+    (tvs, itype') = splitForAllTys itype
+    (_, typeBody) = splitFunTys itype'
+    tys = fromMaybe aAaaOmg $ tyConAppArgs_maybe typeBody
+    aAaaOmg = panicDoc "ToInstance" $ hsep
+      [ "Impossible happened:"
+      , "expected a class constructor in mkNewInstance, but got"
+      , ppr typeBody
+      , "at", ppr $ nameSrcSpan $ getName bindVar
+      ]
+
+
+-- | Go through type applications and apply dictToBare function on `Dict c` type
+unwrapDictExpr :: Type
+                  -- ^ Dict c
+                  --
+                  --   Serves as stop test (if rhs expression matches the type)
+               -> Id
+                  -- ^ dictToBare :: forall (c :: Constraint) . Dict c -> BareConstraint c
+               -> CoreExpr
+                  -- ^ forall a1..an . (Ctx1,.. Ctxn) => Dict c
+               -> Maybe CoreExpr
+                  -- ^ forall a1..an . (Ctx1,.. Ctxn) => BareConstraint c
+unwrapDictExpr dictT unwrapFun ex = case ex of
+    Var _ -> testNWrap Nothing
+    Lit _ -> testNWrap Nothing
+    App e a -> testNWrap $       (App e <$> proceed a)
+                        <|> (flip App a <$> proceed e)
+    Lam b e -> testNWrap $ Lam b <$> proceed e
+    Let b e -> testNWrap $ Let b <$> proceed e
+    Case {} -> testNWrap Nothing
+    Cast {} -> testNWrap Nothing
+    Tick t e -> testNWrap $ Tick t <$> proceed e
+    Type {}  -> Nothing
+    Coercion {} -> Nothing
+  where
+    proceed = unwrapDictExpr dictT unwrapFun
+    testNWrap go = if testType ex then wrap ex else go
+    wrap e = flip fmap (getClsT e) $ \t -> Var unwrapFun `App` t `App` e
+    -- type variables may differ, so I need to use tcMatchTy.
+    -- I do not check if resulting substition is not trivial. Shall I?
+    testType = isJust . Unify.tcMatchTy dictT . exprType
+    getClsT e = case tyConAppArgs_maybe $ exprType e of
+      Just [t] -> Just $ Type t
+      _        -> Nothing
+ test/Spec.hs view
@@ -0,0 +1,231 @@+{-# LANGUAGE CPP               #-}
+{-# LANGUAGE OverloadedStrings #-}
+{-# LANGUAGE QuasiQuotes       #-}
+{-# LANGUAGE RecordWildCards   #-}
+module Main (main) where
+
+import Control.Monad (when)
+import           Data.ByteString       (ByteString)
+import qualified Data.ByteString.Char8 as BS
+import           Data.Char             (isSpace)
+import           Data.Foldable         (fold)
+import           Data.Maybe            (mapMaybe)
+import           Data.Monoid
+import           Data.Traversable      (for)
+import           DynFlags
+import           ErrUtils              (mkLocMessageAnn)
+import           GHC
+import           GHC.Paths             (libdir)
+import           MonadUtils            (liftIO)
+import           Outputable
+import           Path
+import           Path.IO
+import           System.Exit
+import           System.IO
+import           System.FilePath       (isPathSeparator)
+
+-- | Folder with test modules to be compiled
+specDir :: Path Rel Dir
+specDir = [reldir|test/Spec/|]
+
+-- | Folder with expected compiler output dumps
+outDir :: Path Rel Dir
+outDir = [reldir|test/out/|]
+
+correspondingStdOut :: Path a File -> Maybe (Path Rel File)
+correspondingStdOut f = setFileExtension "stdout" $ outDir </> filename f
+
+correspondingStdErr :: Path a File -> Maybe (Path Rel File)
+correspondingStdErr f = setFileExtension "stderr" $ outDir </> filename f
+
+data TargetPaths = TargetPaths
+  { targetName :: String
+  , targetPath :: FilePath
+  , stdoutPath :: FilePath
+  , stderrPath :: FilePath
+  }
+
+lookupTargetPaths :: Path a File -> Maybe TargetPaths
+lookupTargetPaths p = do
+  if fileExtension p == ".hs" then Just () else Nothing
+  targetPath <- Just $ toFilePath p
+  targetName <- toFilePath <$> setFileExtension "" (filename p)
+  stdoutPath <- toFilePath <$> correspondingStdOut p
+  stderrPath <- toFilePath <$> correspondingStdErr p
+  return TargetPaths {..}
+
+
+main :: IO ()
+main = do
+  targetPaths <- mapMaybe lookupTargetPaths <$>
+    (listDir specDir >>= traverse makeRelativeToCurrentDir . snd)
+  withSystemTempFile   "constraints-deriving-stdout" $ \_ outH ->
+    withSystemTempFile "constraints-deriving-stderr" $ \_ errH ->
+    withSystemTempDir  "constraints-deriving-tests"  $ \tempDir -> do
+    r <- defaultErrorHandler defaultFatalMessager defaultFlushOut $
+      runGhc (Just libdir) $ do
+        dflags' <- makeSimpleAndFast <$> getSessionDynFlags
+        (dflags, _, _) <- parseDynamicFlags dflags'
+              { log_action = manualLogAction outH errH}
+          [ noLoc "-Wall"
+          , noLoc "-hide-all-packages"
+          , noLoc "-package ghc"
+          , noLoc "-package base"
+          , noLoc "-package constraints-deriving"
+          , noLoc "-dcore-lint"
+          , noLoc $ "-outputdir " ++ toFilePath tempDir]
+        _ <- setSessionDynFlags dflags
+        ghc800StaticFlagsFix
+        fmap fold $
+          for targetPaths $ \TargetPaths{..} -> do
+            -- compile the module
+            target <- guessTarget targetPath Nothing
+            setTargets [target]
+            outPos <- liftIO $ hGetPosn outH
+            errPos <- liftIO $ hGetPosn errH
+            resCompile <- isSucceeded <$> load LoadAllTargets
+            liftIO $ do
+              -- flush logging handles to make sure logs are written
+              hFlush outH
+              hFlush errH
+              hSetPosn outPos
+              hSetPosn errPos
+              -- compare logs against templates
+              outExpectedBS <- trimBS <$> BS.readFile stdoutPath
+              errExpectedBS <- trimBS <$> BS.readFile stderrPath
+              sameOut <- getSameBytes outExpectedBS outH
+                >>= reportSameBytes targetName "stdout" outExpectedBS
+              sameErr <- getSameBytes errExpectedBS errH
+                >>= reportSameBytes targetName "stderr" errExpectedBS
+              let rez = fold [sameOut, sameErr, resCompile]
+              when (rez == All True) $ do
+                putStrLn ""
+                putStrLn $ targetName ++ ": OK"
+              return rez
+    if getAll r
+    then exitSuccess
+    else exitFailure
+  where
+    isSucceeded Succeeded = All True
+    isSucceeded Failed    = All False
+
+    reportSameBytes _ _ _ SameBytes = pure $ All True
+    reportSameBytes modN ch temBs (Different resBs) = do
+      BS.putStrLn $ BS.unlines
+        [ "", ""
+        , "Failure testing module " `mappend` BS.pack modN `mappend` ":"
+        , "  GHC " `mappend` ch `mappend` " does not match the expected output!"
+        , ""
+        , "---- Expected "  `mappend` ch `mappend` " -----------------------------"
+        , temBs
+        , "---- Content of " `mappend` ch `mappend` " ---------------------------"
+        , resBs
+        , "--------------------------------------------------"
+        , ""
+        ]
+      return $ All False
+
+
+data SameBytes = SameBytes | Different ByteString
+
+-- | Read a ByteString from a handle and compare it to the template
+--
+--   Prerequisite: the template ByteString is trimmed (e.g. using trimBS)
+getSameBytes :: ByteString -> Handle -> IO SameBytes
+getSameBytes template handle =
+    checkSame . trimBS <$> getAvailableBytes (max 1024 (BS.length template + 16))
+  where
+    checkSame bs
+      | eqStar template bs = SameBytes
+      | otherwise          = Different bs
+    getAvailableBytes k = do
+      bs <- BS.hGetNonBlocking handle k
+      if BS.length bs < k
+      then return bs
+      else mappend bs <$> getAvailableBytes (k * 2)
+
+-- | Eliminate whitespace characters on both sides of a ByteString
+trimBS :: ByteString -> ByteString
+trimBS = BS.map f . fst . BS.spanEnd isSpace . snd . BS.span isSpace
+  where
+    -- fix tests for Windows
+    f c = if isPathSeparator c then '/' else c
+
+-- | compare two ByteStrings such that the first can have wildcards '*'
+eqStar :: ByteString -> ByteString -> Bool
+eqStar template bs
+      -- empty output
+    | BS.null template = BS.null bs
+      -- template allows anything
+    | BS.all ('*' ==) template = True
+      -- template starts with a wildcard
+    | BS.null t1 = case BS.breakSubstring t21 bs of
+        (_, bs')
+          | BS.null bs' -> False
+          | otherwise   -> eqStar t22
+                         $ BS.drop (BS.length t21) bs'
+      -- otherwise match prefix
+    | otherwise = case BS.stripPrefix t1 bs of
+        -- could not match
+        Nothing  -> False
+        -- could match a segment, continue
+        Just bs' -> eqStar t2 bs'
+  where
+    (t1 , t2 ) = BS.span ('*' /=) template
+    (t21, t22) = BS.span ('*' /=) $ BS.dropWhile ('*' ==) t2
+
+
+
+makeSimpleAndFast :: DynFlags -> DynFlags
+makeSimpleAndFast flags = flags
+  { ghcMode     = OneShot
+  , ghcLink     = NoLink
+  , verbosity   = 1
+  , optLevel    = 0
+  , ways        = []
+  , useUnicode  = False
+  } `gopt_set` Opt_DoCoreLinting
+    `gopt_set` Opt_ForceRecomp
+    `gopt_unset` Opt_PrintUnicodeSyntax
+
+
+ghc800StaticFlagsFix :: Ghc ()
+#if __GLASGOW_HASKELL__ >= 802
+ghc800StaticFlagsFix = return ()
+#else
+ghc800StaticFlagsFix = do
+  decl <- parseImportDecl "import StaticFlags (initStaticOpts)"
+  setContext [IIDecl decl]
+  _ <- execStmt "initStaticOpts" execOptions
+  return ()
+#endif
+
+-- | I've adapted the defaultLogAction from DynFlags with two goals in mind:
+--
+--   1. Make output as simple as possible (in particular, no utf-8)
+--   2. Redirect stdout and stderr into dedicated handles
+--
+--   These all is to make testing output easy across different GHC versions.
+manualLogAction :: Handle -> Handle -> LogAction
+manualLogAction outH errH dflags _reason severity srcSpan style msg
+    = case severity of
+      SevOutput      -> printOut msg style
+      SevDump        -> printOut (msg $$ blankLine) style
+      SevInteractive -> putStrSDoc msg style
+      SevInfo        -> printErrs msg style
+      SevFatal       -> printErrs msg style
+      SevWarning     -> printWarns
+      SevError       -> printWarns
+  where
+    printOut   = defaultLogActionHPrintDoc  dflags outH
+    printErrs  = defaultLogActionHPrintDoc  dflags errH
+    putStrSDoc = defaultLogActionHPutStrDoc dflags outH
+    message = mkLocMessageAnn Nothing severity srcSpan msg
+    printWarns = do
+      hPutChar errH '\n'
+      printErrs message
+#if __GLASGOW_HASKELL__ >= 802
+        (setStyleColoured False style)
+#else
+        style
+#endif
+ test/Spec/DeriveAll01.hs view
@@ -0,0 +1,24 @@+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.DeriveAll01 where
+
+import Data.Constraint.Deriving
+
+
+data family FooFam a b
+data instance FooFam Int b = FooInt b Int
+  deriving Eq
+data instance FooFam Double b = FooDouble Double b b
+  deriving Read
+data instance FooFam Float Float = FooFloats Float Float
+  deriving (Eq, Ord)
+data instance FooFam Float String = FooString Float String
+  deriving Show
+
+{-# ANN type TestNewtype1 DeriveAll #-}
+newtype TestNewtype1 a b = TestNewtype1C (FooFam a b)
+
+{-# ANN type TestNewtype2 DeriveAll #-}
+newtype TestNewtype2 a b r = TestNewtype2C r
+type instance DeriveContext (TestNewtype2 a b r) = FooFam a b ~ r
+ test/Spec/DeriveAll02.hs view
@@ -0,0 +1,37 @@+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.DeriveAll02 where
+
+import Data.Constraint.Deriving
+
+
+data FooData a b c = FooDataCon Float b
+  deriving (Eq, Ord)
+
+instance (a ~ Int, Show b) => Show (FooData a b c) where
+  show (FooDataCon f b) = "FooDataCon " ++ show f ++ " " ++ show b
+
+
+type family FooFam a b c d e f
+type instance FooFam a b c Double e f = FooData Int b c
+
+class Ord b => FooClass a b c where
+  fooFun :: a -> b -> c
+  barFun :: a -> c -> b
+
+instance (a ~ Int, Ord b, Show a) => FooClass (FooData a b c) b Float where
+  fooFun (FooDataCon f _) _ = f
+  barFun (FooDataCon _ b) _ = b
+
+
+{-# ANN type BazTy DeriveAll #-}
+newtype BazTy a b c d e f = BazCon (FooFam a b c d e f)
+
+-- Type class constraints are prepended to the instance arguments.
+-- Thus, they can be used to impose additional (fictional) constraints
+-- on the generated instances.
+type instance DeriveContext (BazTy a b c d e f ) = Show e
+ test/Spec/DeriveAll03.hs view
@@ -0,0 +1,34 @@+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE TypeFamilyDependencies #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.DeriveAll03 where
+
+import Data.Constraint.Deriving
+
+{-
+  Here I test three different things:
+
+  * Deriving instances for the types defined elsewhere
+    (including the base library);
+    it should produce a lot of instances for all transitively
+    reachable modules.
+
+  * Closed, injective type families - should not be a problem.
+
+  * Higher-kinded types;
+    The following should produce instances for kind `Type`
+     (e.g. Show, Monoid)
+    as well as for kind `Type -> Type`
+     (e.g. Functor, Monad)
+ -}
+data ListTy
+data MaybeTy
+
+type family FooFam m = r | r -> m where
+  FooFam ListTy = []
+  FooFam MaybeTy = Maybe
+
+{-# ANN type BazTy DeriveAll #-}
+newtype BazTy m a = BazCon (FooFam m a)
+ test/Spec/DeriveAll04.hs view
@@ -0,0 +1,20 @@+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.DeriveAll04 where
+
+import Data.Constraint.Deriving
+
+{-
+  Here, I want to test overlapping type families and their wildcards
+ -}
+
+data A = ACon deriving Eq
+data B = BCon deriving Eq
+
+type family AB x where
+  AB A = A
+  AB _ = B
+
+{-# ANN type BazTy DeriveAll #-}
+newtype BazTy a = BazCon (AB a)
+ test/Spec/DeriveAll05.hs view
@@ -0,0 +1,13 @@+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.DeriveAll05 where
+
+import Data.Constraint.Deriving
+
+data family AB x
+data instance AB _ = B deriving Eq
+
+{-# ANN type BazTy DeriveAll #-}
+newtype BazTy a = BazCon (AB a)
+
+ test/Spec/ToInstance01.hs view
@@ -0,0 +1,51 @@+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# OPTIONS_GHC -fplugin Data.Constraint.Deriving #-}
+{-# OPTIONS_GHC -fplugin-opt Data.Constraint.Deriving:dump-instances #-}
+module Spec.ToInstance01 where
+
+{-
+This is a minimal example for deriving multiple instances
+for a newtype over a type family.
+
+The plugin provides two advantages over manually implementing instances using singletons:
+
+  * No need to implement every class function manually
+
+  * Instance elaboration at the call site happens only once for many used functions,
+    rather than once for every fuction usage.
+ -}
+import Data.Constraint
+import Data.Constraint.Unsafe
+import Data.Constraint.Deriving
+
+newtype Number t = Number (NumberFam t)
+
+type family NumberFam t where
+  NumberFam Int = Int
+  NumberFam Double = Double
+
+data NumberSing t where
+  NumInt    :: NumberSing Int
+  NumDouble :: NumberSing Double
+
+class    KnownNumber t      where numberSing :: NumberSing t
+instance KnownNumber Int    where numberSing = NumInt
+instance KnownNumber Double where numberSing = NumDouble
+
+{-# ANN deriveEq (ToInstance NoOverlap) #-}
+deriveEq :: KnownNumber t => Dict (Eq (Number t))
+deriveEq = deriveIt numberSing
+
+{-# ANN deriveOrd (ToInstance NoOverlap) #-}
+deriveOrd :: KnownNumber t => Dict (Ord (Number t))
+deriveOrd = deriveIt numberSing
+
+{-# ANN deriveNum (ToInstance NoOverlap) #-}
+deriveNum :: KnownNumber t => Dict (Num (Number t))
+deriveNum = deriveIt numberSing
+
+deriveIt :: (c Double, c Int) => NumberSing t -> Dict (c (Number t)) 
+deriveIt NumInt    = mapDict (unsafeDerive Number) Dict
+deriveIt NumDouble = mapDict (unsafeDerive Number) Dict
+ test/out/DeriveAll01.stderr view
@@ -0,0 +1,31 @@+============ Class instances declared in this module ============
+  instance Eq b => Eq (FooFam Int b)
+    -- Defined at test/Spec/DeriveAll01.hs:*
+  instance Eq (FooFam Float Float)
+    -- Defined at test/Spec/DeriveAll01.hs:*
+  instance Eq b => Eq (TestNewtype1 Int b)
+    -- Defined in `Spec.DeriveAll01'
+  instance Eq (TestNewtype1 Float Float)
+    -- Defined in `Spec.DeriveAll01'
+  instance Eq b => Eq (TestNewtype2 Int b (FooFam Int b))
+    -- Defined in `Spec.DeriveAll01'
+  instance Eq (TestNewtype2 Float Float (FooFam Float Float))
+    -- Defined in `Spec.DeriveAll01'
+  instance Ord (FooFam Float Float)
+    -- Defined at test/Spec/DeriveAll01.hs:*
+  instance Ord (TestNewtype1 Float Float)
+    -- Defined in `Spec.DeriveAll01'
+  instance Ord (TestNewtype2 Float Float (FooFam Float Float))
+    -- Defined in `Spec.DeriveAll01'
+  instance Read b => Read (FooFam Double b)
+    -- Defined at test/Spec/DeriveAll01.hs:*
+  instance Read b => Read (TestNewtype1 Double b)
+    -- Defined in `Spec.DeriveAll01'
+  instance Read b => Read (TestNewtype2 Double b (FooFam Double b))
+    -- Defined in `Spec.DeriveAll01'
+  instance Show (FooFam Float String)
+    -- Defined at test/Spec/DeriveAll01.hs:*
+  instance Show (TestNewtype1 Float [Char])
+    -- Defined in `Spec.DeriveAll01'
+  instance Show (TestNewtype2 Float [Char] (FooFam Float String))
+    -- Defined in `Spec.DeriveAll01'
+ test/out/DeriveAll01.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.DeriveAll01 ( test/Spec/DeriveAll01.hs, * )
+ test/out/DeriveAll02.stderr view
@@ -0,0 +1,14 @@+============ Class instances declared in this module ============
+  instance (Show e, Eq b) => Eq (BazTy a b c Double e f)
+    -- Defined in `Spec.DeriveAll02'
+  instance Eq b => Eq (FooData a b c)
+    -- Defined at test/Spec/DeriveAll02.hs:*
+  instance (a ~ Int, Ord b, Show a) =>
+           FooClass (FooData a b c) b Float
+    -- Defined at test/Spec/DeriveAll02.hs:*
+  instance (Show e, Ord b) => Ord (BazTy a b c Double e f)
+    -- Defined in `Spec.DeriveAll02'
+  instance Ord b => Ord (FooData a b c)
+    -- Defined at test/Spec/DeriveAll02.hs:*
+  instance (a ~ Int, Show b) => Show (FooData a b c)
+    -- Defined at test/Spec/DeriveAll02.hs:*
+ test/out/DeriveAll02.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.DeriveAll02 ( test/Spec/DeriveAll02.hs, * )
+ test/out/DeriveAll03.stderr view
@@ -0,0 +1,25 @@+============ Class instances declared in this module ============
+  instance *Alternative (BazTy ListTy)*
+  instance *Alternative (BazTy MaybeTy)*
+  instance *Applicative (BazTy ListTy)*
+  instance *Applicative (BazTy MaybeTy)*
+  instance Eq a => Eq (BazTy ListTy a)*
+  instance Eq a => Eq (BazTy MaybeTy a)*
+  instance Foldable (BazTy ListTy)*
+  instance Foldable (BazTy MaybeTy)*
+  instance Functor (BazTy ListTy)*
+  instance Functor (BazTy MaybeTy)*
+  instance *Monad (BazTy ListTy)*
+  instance *Monad (BazTy MaybeTy)*
+  instance *MonadPlus (BazTy ListTy)*
+  instance *MonadPlus (BazTy MaybeTy)*
+  instance *Monoid (BazTy ListTy a)*
+  instance *Monoid (BazTy MaybeTy a)*
+  instance Ord a => Ord (BazTy ListTy a)*
+  instance Ord a => Ord (BazTy MaybeTy a)*
+  instance Read a => Read (BazTy ListTy a)*
+  instance Read a => Read (BazTy MaybeTy a)*
+  instance Show a => Show (BazTy ListTy a)*
+  instance Show a => Show (BazTy MaybeTy a)*
+  instance Traversable (BazTy ListTy)*
+  instance Traversable (BazTy MaybeTy)*
+ test/out/DeriveAll03.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.DeriveAll03 ( test/Spec/DeriveAll03.hs, * )
+ test/out/DeriveAll04.stderr view
@@ -0,0 +1,7 @@+============ Class instances declared in this module ============
+  instance Eq A -- Defined at test/Spec/DeriveAll04.hs:*
+  instance Eq B -- Defined at test/Spec/DeriveAll04.hs:*
+  instance [overlapping] Eq (BazTy A)
+    -- Defined in `Spec.DeriveAll04'
+  instance [incoherent] Eq (BazTy fresh_*)
+    -- Defined in `Spec.DeriveAll04'
+ test/out/DeriveAll04.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.DeriveAll04 ( test/Spec/DeriveAll04.hs, * )
+ test/out/DeriveAll05.stderr view
@@ -0,0 +1,3 @@+============ Class instances declared in this module ============
+  instance Eq (AB _) -- Defined at test/Spec/DeriveAll05.hs:*
+  instance Eq (BazTy a) -- Defined in `Spec.DeriveAll05'
+ test/out/DeriveAll05.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.DeriveAll05 ( test/Spec/DeriveAll05.hs, * )
+ test/out/ToInstance01.stderr view
@@ -0,0 +1,11 @@+============ Class instances declared in this module ============
+  instance KnownNumber t => Eq (Number t)
+    -- Defined in `Spec.ToInstance01'
+  instance KnownNumber Double
+    -- Defined at test/Spec/ToInstance01.hs:*
+  instance KnownNumber Int
+    -- Defined at test/Spec/ToInstance01.hs:*
+  instance KnownNumber t => Num (Number t)
+    -- Defined in `Spec.ToInstance01'
+  instance KnownNumber t => Ord (Number t)
+    -- Defined in `Spec.ToInstance01'
+ test/out/ToInstance01.stdout view
@@ -0,0 +1,1 @@+[*] Compiling Spec.ToInstance01 ( test/Spec/ToInstance01.hs, * )