diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,17 @@
+# Changelog for `ghc-magic-dict-compat`
+
+All notable changes to this project will be documented in this file.
+
+The format is based on [Keep a Changelog](https://keepachangelog.com/en/1.0.0/),
+and this project adheres to the
+[Haskell Package Versioning Policy](https://pvp.haskell.org/).
+
+## 0.0.0.0 - 2023-12-31
+
+### Added
+
+- First Release
+
+## Unreleased
+
+## 0.1.0.0 - YYYY-MM-DD
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,30 @@
+Copyright Hiromi ISHII (c) 2023
+
+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 Hiromi ISHII nor the names of other
+      contributors may be used to endorse or promote products derived
+      from this software without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,56 @@
+# ghc-magic-dict-compat - A compatibility layer and GHC Plugin for `withDict` magic function
+
+Since GHC 9.4, the compiler provides magic type-class `WithDict` and its member function `withDict`:
+
+```haskell
+withDict :: 
+  forall cls meth {rr} (r :: Type rr).
+  WithDict cls meth =>
+  meth ->
+  (cls => r) ->
+  r
+```
+
+This is the much safer version of `unsafeCoerce` to (unsafely) produce an instance dictionary for singleton classes dynamically - the compiler checks the preconditions statically at the compile time. Although it is potentially unsafe, this combinator is particularly useful when one writes the library manipulating instance dictionary dynamically.
+
+This package provides a thin compatibility layer for `withDict` from `GHC.Magic.Dict` for GHC <9.4.
+The package consists of the following two modules:
+
+- `GHC.Magic.Dict.Compat`
+- `GHC.Magic.Dict.Plugin`
+
+All you have to do is to import `GHC.Magic.Dict.Compat` and put the following at the top of modules calling `withDict`:
+
+```haskell
+{-# OPTIONS_GHC -fplugin GHC.Magic.Dict.Plugin #-}
+```
+
+`GHC.Magic.Dict.Compat` provides a type-class `WithDict` and `withDict` combinator for GHC <9.4; it just re-expose them for GHC >= 9.4.
+For GHC <9.4, user-facing API is almost the same, except for `withDict` is _not_ a member function of `WithDict`.
+This is to prevent user-defined instances of `WithDict` by imposing unsolvable default signatures for hidden member functions.
+Still, users can refer to `WithDict` the constraint and use `withDict` function almost the same way as in GHC >=9.4, so this subtle difference should not be a big problem.
+
+As users cannot define the instance of `WithDict` manually, the `GHC.Magic.Dict.Compat` module alone is not enough.
+Here, the GHC Plugin `GHC.Magic.Dict.Plugin` comes into play. For GHC <9.4, the plugin generates the dictionary for `WithDict` dynamically at the compile time, employing the almost the same logic as GHC >= 9.4. For newer GHC, it does no-op.
+
+## Usage
+
+1. Import `withDict` (and `WithDict` if necessary) from `GHC.Magic.Dict.Compat`
+2. Enable GHC Plugin `GHC.Magic.Dict.Plugin` either by placing `{-# GHC_OPTIONS -fplugin GHC.Magic.Dict.Plugin #-}` at the top or adding `-fplugin GHC.Magic.Dict.Plugin` to `ghc-options` of the package.
+
+With this, you can freely use `withDict` both with GHC <9.4 and >=9.4.
+
+### Example
+
+```hs
+{-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications, ConstraintKinds #-}
+{-# GHC_OPTIONS -fplugin GHC.Magic.Dict.Plugin #-}
+module MyModule where
+import GHC.Magic.Dict.Compat
+
+class Given a where
+  given :: a
+
+give :: a -> (Given a => r) -> r
+give = withDict @(Given a) @a
+```
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,2 @@
+import Distribution.Simple
+main = defaultMain
diff --git a/ghc-magic-dict-compat.cabal b/ghc-magic-dict-compat.cabal
new file mode 100644
--- /dev/null
+++ b/ghc-magic-dict-compat.cabal
@@ -0,0 +1,79 @@
+cabal-version:      1.12
+name:               ghc-magic-dict-compat
+version:            0.0.0.0
+category:           Type System, Compatibility
+synopsis:
+  A compatibility layer and GHC plugin for `withDict` from "GHC.Magic.Dict".
+
+description:
+  Please see the README on GitHub at <https://github.com/konn/ghc-magic-dict-compat#readme>
+
+homepage:           https://github.com/konn/ghc-magic-dict-compat#readme
+bug-reports:        https://github.com/konn/ghc-magic-dict-compat/issues
+author:             Hiromi ISHII
+maintainer:         konn.jinro_at_gmail.com
+copyright:          2023 (c) Hiromi ISHII
+license:            BSD3
+license-file:       LICENSE
+build-type:         Simple
+extra-source-files:
+  CHANGELOG.md
+  README.md
+
+source-repository head
+  type:     git
+  location: https://github.com/konn/ghc-magic-dict-compat
+
+library
+  exposed-modules:
+    GHC.Magic.Dict.Compat
+    GHC.Magic.Dict.Plugin
+
+  other-modules:    GHC.TypeError.Compat
+
+  if impl(ghc <9.4)
+    other-modules: GHC.Magic.Dict.Plugin.Old
+
+  other-modules:    Paths_ghc_magic_dict_compat
+  hs-source-dirs:   src
+  ghc-options:
+    -Wall -Wcompat -Widentities -Wincomplete-record-updates
+    -Wincomplete-uni-patterns -Wmissing-export-lists
+    -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+
+  build-depends:
+      base                 >=4.7 && <5
+    , dlist
+    , ghc
+    , ghc-prim
+    , ghc-tcplugins-extra
+
+  default-language: Haskell2010
+
+test-suite ghc-magic-dict-compat-test
+  type:               exitcode-stdio-1.0
+  main-is:            Spec.hs
+  other-modules:
+    GHC.Magic.Dict.CompatSpec
+    GHC.Magic.Dict.Defs
+    GHC.Magic.Dict.Errors
+    GHC.Magic.Dict.Goods
+    Paths_ghc_magic_dict_compat
+
+  hs-source-dirs:     test
+  ghc-options:
+    -fobject-code -Wall -Wcompat -Widentities
+    -Wincomplete-record-updates -Wincomplete-uni-patterns
+    -Wmissing-export-lists -Wmissing-home-modules -Wpartial-fields
+    -Wredundant-constraints -threaded -rtsopts -with-rtsopts=-N
+
+  build-tool-depends: tasty-discover:tasty-discover -any
+  build-depends:
+      base                   >=4.7 && <5
+    , falsify
+    , ghc-magic-dict-compat
+    , tasty
+    , tasty-discover
+    , tasty-hunit
+
+  default-language:   Haskell2010
diff --git a/src/GHC/Magic/Dict/Compat.hs b/src/GHC/Magic/Dict/Compat.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Magic/Dict/Compat.hs
@@ -0,0 +1,83 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE DefaultSignatures #-}
+{-# LANGUAGE FlexibleContexts #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE Unsafe #-}
+{-# LANGUAGE NoImplicitPrelude #-}
+
+{- |
+This module provides a compatibility layer of 'withDict' and 'WithDict' for GHC <9.4.
+For GHC \<9.4, the definitions of 'WithDict' and 'withDict' are slightly different from those of GHC \>= 9.4 to prevent user-defined instances.
+
+To actually make 'withDict' work, you have to invoke the accompanying GHC Plugin exposed from "GHC.Magic.Dict.Plugin". For example:
+
+@
+{\-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications, ConstraintKinds #-\}
+{\-# GHC_OPTIONS -fplugin "GHC.Magic.Dict.Plugin" #-\}
+module MyModule where
+import "GHC.Magic.Dict.Compat"
+
+class Given a where
+  given :: a
+
+give :: a -> (Given a => r) -> r
+give = 'withDict' \@(Given a) \@a
+@
+
+For GHC \>=9.4, this module just re-exports the module "GHC.Magic.Dict" and the plugin is just a no-op - so you can safely use this package without concerning break anything in newer GHCs.
+-}
+module GHC.Magic.Dict.Compat (
+  WithDict,
+  withDict,
+) where
+
+#if MIN_VERSION_ghc_prim(0,9,0)
+import GHC.Magic.Dict (WithDict(), withDict)
+#else
+
+import GHC.TypeError.Compat (Unsatisfiable, unsatisfiable)
+import GHC.TypeLits
+import GHC.Types (RuntimeRep, TYPE)
+
+class WithDict cls meth where
+  withDict_ :: forall {rr :: RuntimeRep} (r :: TYPE rr). meth -> ((cls) => r) -> r
+  default withDict_ ::
+    ( Unsatisfiable
+        ( 'Text "Class `"
+            ':<>: 'ShowType WithDict
+            ':<>: 'Text " does not support user-specified-instances."
+            ':$$: 'Text "In the instance declaration for `"
+            ':<>: 'ShowType (WithDict cls meth)
+            ':<>: 'Text "'"
+        )
+    ) =>
+    forall {rr :: RuntimeRep} (r :: TYPE rr).
+    meth ->
+    ((cls) => r) ->
+    r
+  withDict_ = unsatisfiable
+
+-- | @'withDict' d f@ provides a way to call a type-class–overloaded function
+--   @f@ by applying it to the supplied dictionary @d@.
+--
+--   'withDict' can only be used if the type class has a single method with no
+--   superclasses. For more (important) details on how this works, see
+--   @Note [withDict]@ in "GHC.Tc.Instance.Class" in GHC.
+withDict ::
+  forall cls meth {rr :: RuntimeRep} (r :: TYPE rr).
+  (WithDict cls meth) =>
+  meth ->
+  ((cls) => r) ->
+  r
+{-# INLINE withDict #-}
+withDict = withDict_ @cls @meth
+#endif
diff --git a/src/GHC/Magic/Dict/Plugin.hs b/src/GHC/Magic/Dict/Plugin.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Magic/Dict/Plugin.hs
@@ -0,0 +1,39 @@
+{-# LANGUAGE CPP #-}
+
+{- |
+A type-checker plugin to resolve 'WithDict' constraints for GHC \<9.4; it is just a no-op for GHC >=9.4.
+
+This plugin is inteded to be used with the compatibility layer exposed from "GHC.Magic.Dict.Compat".
+For GHC \<9.4, the definitions of 'GHC.Magic.Dict.Compat.WithDict' and 'GHC.Magic.Dict.Compat.withDict' are slightly different from those of GHC \>= 9.4 to prevent user-defined instances.
+
+Example usage:
+
+@
+{\-# LANGUAGE RankNTypes, ScopedTypeVariables, TypeApplications, ConstraintKinds #-\}
+{\-# GHC_OPTIONS -fplugin GHC.Magic.Dict.Plugin #-\}
+module MyModule where
+import "GHC.Magic.Dict.Compat"
+
+class Given a where
+  given :: a
+
+give :: a -> (Given a => r) -> r
+give = 'GHC.Magic.Dict.Compat.withDict' \@(Given a) \@a
+@
+
+For GHC \>=9.4, this module just re-exports the module "GHC.Magic.Dict" and the plugin is just a no-op - so you can safely use this package without concerning break anything in newer GHCs.
+-}
+module GHC.Magic.Dict.Plugin (plugin) where
+
+import GHC.Plugins (Plugin)
+#if MIN_VERSION_ghc(9,4,0)
+import GHC.Plugins (defaultPlugin, pluginRecompile, purePlugin)
+
+plugin :: Plugin
+plugin = defaultPlugin { pluginRecompile = purePlugin }
+#else
+import qualified GHC.Magic.Dict.Plugin.Old as Old
+
+plugin :: Plugin
+plugin = Old.plugin
+#endif
diff --git a/src/GHC/Magic/Dict/Plugin/Old.hs b/src/GHC/Magic/Dict/Plugin/Old.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/Magic/Dict/Plugin/Old.hs
@@ -0,0 +1,149 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE RecordWildCards #-}
+{-# LANGUAGE TupleSections #-}
+
+module GHC.Magic.Dict.Plugin.Old (plugin) where
+
+import Control.Applicative (liftA2)
+import Data.Bitraversable (bitraverse)
+import qualified Data.DList as DL
+import Data.Maybe (mapMaybe)
+import GHC.Builtin.Types.Prim (openAlphaTy, openAlphaTyVar, runtimeRep1TyVar)
+import qualified GHC.Core as Core
+import GHC.Core.Class
+import GHC.Core.Coercion (mkSubCo, mkSymCo, mkTransCo)
+import GHC.Core.DataCon
+import GHC.Core.Make (mkCoreLams)
+import GHC.Core.Predicate
+import GHC.Core.TyCon
+import GHC.Core.Type
+import GHC.Data.FastString
+import GHC.Plugins (Plugin (..), defaultPlugin, mkModuleName, purePlugin)
+import GHC.Tc.Instance.Family (tcInstNewTyCon_maybe)
+import GHC.Tc.Plugin hiding (newWanted)
+import GHC.Tc.Types
+import GHC.Tc.Types.Constraint
+import GHC.Tc.Types.Evidence
+import GHC.TcPluginM.Extra
+import GHC.Types.Id
+import GHC.Types.Name
+import GHC.Utils.Outputable
+
+plugin :: Plugin
+plugin =
+  defaultPlugin
+    { tcPlugin = const $ Just withDictPlugin
+    , pluginRecompile = purePlugin
+    }
+
+withDictPlugin :: TcPlugin
+withDictPlugin =
+  tracePlugin
+    "WithDictPlugin"
+    TcPlugin
+      { tcPluginStop = const $ pure ()
+      , tcPluginSolve = const solveWithDict
+      , tcPluginInit = pure ()
+      }
+
+data Info = Info
+  { _WithDict :: !Class
+  , _WithDictDataCon :: !DataCon
+  }
+
+solveWithDict :: TcPluginSolver
+solveWithDict _ _ [] = pure $ TcPluginOk [] []
+solveWithDict gs _ wanteds = do
+  let subs = map fst $ mkSubst' gs
+  info <- lookupInfo
+  let withDicts =
+        mapMaybe
+          ( liftA2 (,)
+              <$> (liftA2 (,) <$> pure . ctLoc <*> decodeWithDictPred info . ctPred . substCt subs)
+              <*> pure
+          )
+          wanteds
+  (contrs, solved, wants) <-
+    foldMap
+      ( \case
+          (Nothing, ct) -> (DL.singleton ct, mempty, mempty)
+          (Just (pf, newWants), ct) -> (mempty, DL.singleton (pf, ct), DL.fromList newWants)
+      )
+      <$> mapM (bitraverse (uncurry $ solveWithDictPred info) pure) withDicts
+  tcPluginTrace
+    "solveWithDict/contradictions"
+    (ppr $ DL.toList contrs)
+  tcPluginTrace "solveWithDict/solveds" $ ppr $ DL.toList solved
+  tcPluginTrace "solveWithDict/newWanteds" $ ppr $ DL.toList wants
+  pure $
+    if null contrs
+      then TcPluginOk (DL.toList solved) (DL.toList wants)
+      else TcPluginContradiction $ DL.toList contrs
+
+mkNonCanonical' ::
+  CtLoc -> CtEvidence -> Ct
+mkNonCanonical' origCtl ev =
+  let ct_ls = ctLocSpan origCtl
+      ctl = ctEvLoc ev
+      wanted = mkNonCanonical ev
+   in setCtLoc wanted (setCtLocSpan ctl ct_ls)
+
+solveWithDictPred :: Info -> CtLoc -> DecodedPred -> TcPluginM (Maybe (EvTerm, [Ct]))
+solveWithDictPred Info {..} loc DecodedPred {..} = do
+  tcPluginTrace "solveWithDictPred" (ppr (constraint, argType))
+  case tcInstNewTyCon_maybe constrTyCon constrArgs of
+    Nothing -> do
+      tcPluginTrace "solveWithDictPred: Failed!" (ppr (constraint, argType))
+      pure Nothing
+    Just (onlyMethodType, co) -> do
+      tcPluginTrace "solveWithDictPred: singleton class found" (ppr (constraint, argType, onlyMethodType, co))
+      let nomEq = mkPrimEqPred argType onlyMethodType
+      hole <- newCoercionHole nomEq
+      let want = CtWanted nomEq (HoleDest hole) WDeriv loc
+      sv <- unsafeTcPluginTcM $ mkSysLocalM (fsLit "withDict_s") Many argType
+      k <- unsafeTcPluginTcM $ mkSysLocalM (fsLit "withDict_k") Many (mkInvisFunTy Many constraint openAlphaTy)
+      -- Given co2 : mty ~N# inst_meth_ty, construct the method of
+      -- the WithDict dictionary:
+      --
+      --   \@(r :: RuntimeRep) @(a :: TYPE r) (sv :: mty) (k :: cls => a) ->
+      --     k (sv |> (sub co ; sym co2))
+      let proof =
+            evDataConApp
+              _WithDictDataCon
+              [constraint, argType]
+              [ mkCoreLams [runtimeRep1TyVar, openAlphaTyVar, sv, k] $
+                  Core.Var k
+                    `Core.App` (Core.Var sv `Core.Cast` mkTransCo (mkSubCo (ctEvCoercion want)) (mkSymCo co))
+              ]
+      pure $ Just (proof, [mkNonCanonical' loc want])
+
+data DecodedPred = DecodedPred
+  { constraint :: !PredType
+  , constrTyCon :: !TyCon
+  , constrArgs :: ![Type]
+  , argType :: !Type
+  }
+
+decodeWithDictPred :: Info -> PredType -> Maybe DecodedPred
+decodeWithDictPred Info {..} pt
+  | ClassPred withDic [cls, argType] <- classifyPredType pt
+  , withDic == _WithDict
+  , Just (dict_tc, dict_args) <- tcSplitTyConApp_maybe cls =
+      pure
+        DecodedPred
+          { constraint = cls
+          , constrTyCon = dict_tc
+          , constrArgs = dict_args
+          , ..
+          }
+  | otherwise = Nothing
+
+lookupInfo :: TcPluginM Info
+lookupInfo = do
+  theMod <-
+    lookupModule
+      (mkModuleName "GHC.Magic.Dict.Compat")
+      (fsLit "ghc-magic-dict-compat")
+  _WithDict <- tcLookupClass =<< lookupOrig theMod (mkTcOcc "WithDict")
+  let _WithDictDataCon = classDataCon _WithDict
+  pure Info {..}
diff --git a/src/GHC/TypeError/Compat.hs b/src/GHC/TypeError/Compat.hs
new file mode 100644
--- /dev/null
+++ b/src/GHC/TypeError/Compat.hs
@@ -0,0 +1,30 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE EmptyCase #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# LANGUAGE UndecidableSuperClasses #-}
+
+module GHC.TypeError.Compat (Unsatisfiable, unsatisfiable) where
+
+#if MIN_VERSION_base(4,19,0)
+import GHC.TypeError  (Unsatisfiable, unsatisfiable)
+#else
+import Data.Void (Void)
+import GHC.Exts
+import GHC.TypeLits
+
+class Any => Bottom where
+  unsatisfiable' :: Void
+
+class (Bottom, TypeError e) => Unsatisfiable e
+instance (Bottom, TypeError e) => Unsatisfiable e
+
+unsatisfiable :: forall {rep} (a :: TYPE rep). (Bottom) => a
+unsatisfiable = case unsatisfiable' of {}
+#endif
diff --git a/test/GHC/Magic/Dict/CompatSpec.hs b/test/GHC/Magic/Dict/CompatSpec.hs
new file mode 100644
--- /dev/null
+++ b/test/GHC/Magic/Dict/CompatSpec.hs
@@ -0,0 +1,107 @@
+{-# LANGUAGE LambdaCase #-}
+{-# LANGUAGE TypeApplications #-}
+{-# LANGUAGE ViewPatterns #-}
+
+module GHC.Magic.Dict.CompatSpec (test_fails, test_successes) where
+
+import Control.Exception
+import Data.Char (chr, ord)
+import Data.Function (on)
+import GHC.Magic.Dict.Defs
+import GHC.Magic.Dict.Errors
+import GHC.Magic.Dict.Goods
+import qualified Test.Falsify.Generator as F
+import Test.Falsify.Predicate ((.$))
+import qualified Test.Falsify.Predicate as P
+import qualified Test.Falsify.Range as F
+import Test.Tasty
+import Test.Tasty.Falsify (testProperty)
+import qualified Test.Tasty.Falsify as F
+import Test.Tasty.HUnit
+
+newtype OpaqueInt = OpaqueInt {getInt :: Int}
+
+test_fails :: TestTree
+test_fails =
+  testGroup
+    "Must type error"
+    [ testCase "withEqFail" $ expectTypeError $ withEqFail @OpaqueInt ((==) `on` getInt) ((==) @OpaqueInt)
+    , testCase "badClass1 (unsaturated)" $ expectTypeError badClass1
+    , testCase "badClass1" $ expectTypeError (badClass1 42)
+    , testCase "badClass2 (unsaturated)" $ expectTypeError badClass2
+    , testCase "badClass2" $ expectTypeError (badClass2 42 34)
+    , testCase "badVoid" $ expectTypeError badVoid
+    ]
+
+expectTypeError :: a -> Assertion
+expectTypeError ans =
+  try (evaluate ans) >>= \case
+    Left (fromException -> Just TypeError {}) -> pure ()
+    Left e -> assertFailure $ "Expected TypeError, got " <> show e
+    Right _ -> assertFailure "Expected TypeError, got no exception"
+
+test_successes :: TestTree
+test_successes =
+  testGroup
+    "Must pass"
+    [ testProperty "eq2MyEqInt === (==) @Int" $ do
+        i <- F.gen $ F.int $ F.between (minBound, maxBound)
+        j <- F.gen $ F.int $ F.between (minBound, maxBound)
+        F.assert $ P.expect (i == j) .$ ("result", eq2MyEqInt i j)
+    , testProperty "neq2MyEqInt === (/=) @Int" $ do
+        i <- F.gen $ F.int $ F.between (minBound, maxBound)
+        j <- F.gen $ F.int $ F.between (minBound, maxBound)
+        F.assert $ P.expect (i /= j) .$ ("result", neq2MyEqInt i j)
+    , testProperty "eq2MyEqPoly @Bool === (==) @Bool" $ do
+        i <- F.gen $ F.bool False
+        j <- F.gen $ F.bool False
+        F.assert $ P.expect (i == j) .$ ("result", eq2MyEqPoly i j)
+    , testProperty "eq2MyEqPoly @Bool === (/=) @Bool" $ do
+        i <- F.gen $ F.bool False
+        j <- F.gen $ F.bool False
+        F.assert $ P.expect (i /= j) .$ ("result", neq2MyEqPoly i j)
+    , testProperty "unRelatedBy (\\i c -> i == ord c) === (i /= ord c)" $ do
+        i <- F.gen $ F.int $ F.between (0, 255)
+        j <- F.gen $ chr <$> F.int (F.between (0, 255))
+        F.assert $ P.expect (i /= ord j) .$ ("result", unRelatedBy (\n c -> n == ord c) i j)
+    , testProperty "unRelatedBy @(Bool, Bool) @Bool r === fmap not . r" $ do
+        F.Fn2 rel <- F.gen $ F.fun $ F.bool False
+        p <- F.gen $ F.bool False
+        q <- F.gen $ F.bool False
+        F.assert $
+          P.expect (not $ rel p q)
+            .$ ("result", unRelatedBy rel p q)
+    , testProperty "give i given == i" $ do
+        i <- F.gen $ F.int $ (-128, 128) `F.withOrigin` 0
+        F.assert $ P.expect i .$ ("result", give i given)
+    , testProperty "give i (give j given) == i" $ do
+        i <-
+          F.genWith (Just . ("i = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        j <-
+          F.genWith (Just . ("j = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        F.assert $ P.expect i .$ ("result", give i (give j given))
+    , testProperty "give i (given, give j given) == (i, i)" $ do
+        i <-
+          F.genWith (Just . ("i = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        j <-
+          F.genWith (Just . ("j = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        F.assert $ P.expect (i, i) .$ ("result", give i (given, give j given))
+    , testProperty "(give i given, give j given) == (i, j)" $ do
+        i <-
+          F.genWith (Just . ("i = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        j <-
+          F.genWith (Just . ("j = " <>) . show) $
+            F.int $
+              (-128, 128) `F.withOrigin` 0
+        F.assert $ P.expect (i, j) .$ ("result", (give i given, give j given))
+    ]
diff --git a/test/GHC/Magic/Dict/Defs.hs b/test/GHC/Magic/Dict/Defs.hs
new file mode 100644
--- /dev/null
+++ b/test/GHC/Magic/Dict/Defs.hs
@@ -0,0 +1,32 @@
+{-# LANGUAGE MultiParamTypeClasses #-}
+
+module GHC.Magic.Dict.Defs (
+  MyEq (..),
+  Related (..),
+  BadClass1 (..),
+  BadClass2 (),
+  badeq2,
+  Inhabited (..),
+  Given (..),
+) where
+
+class MyEq a where
+  eq :: a -> a -> Bool
+
+class Related a b where
+  related :: a -> b -> Bool
+
+class BadClass1 a where
+  pos :: a -> a
+  neg :: a -> a
+
+class (MyEq a) => BadClass2 a
+
+badeq2 :: (BadClass2 a) => a -> a -> Bool
+badeq2 = eq
+
+class Inhabited a where
+  inhibitant :: a
+
+class Given a where
+  given :: a
diff --git a/test/GHC/Magic/Dict/Errors.hs b/test/GHC/Magic/Dict/Errors.hs
new file mode 100644
--- /dev/null
+++ b/test/GHC/Magic/Dict/Errors.hs
@@ -0,0 +1,31 @@
+{-# LANGUAGE CPP #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -Wno-orphans #-}
+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors -dcore-lint #-}
+{-# OPTIONS_GHC -fplugin GHC.Magic.Dict.Plugin #-}
+
+module GHC.Magic.Dict.Errors (badClass1, badClass2, badVoid, withEqFail) where
+
+import Data.Void (Void)
+import GHC.Magic.Dict.Compat
+import GHC.Magic.Dict.Defs
+
+withEqFail :: forall a r. (a -> a -> Bool) -> ((Eq a) => r) -> r
+withEqFail = withDict @(Eq a)
+
+badClass1 :: Int -> Int
+badClass1 = withDict @(BadClass1 Int) (id @Int) neg
+
+badClass2 :: Int -> Int -> Bool
+badClass2 = withDict @(BadClass2 Int) ((==) @Int) badeq2
+
+#if defined(__GLASGOW_HASKELL__) && __GLASGOW_HASKELL__ < 904
+instance WithDict (Inhabited Void) ()
+#endif
+
+badVoid :: Void
+badVoid = withDict @(Inhabited Void) () (inhibitant @Void)
diff --git a/test/GHC/Magic/Dict/Goods.hs b/test/GHC/Magic/Dict/Goods.hs
new file mode 100644
--- /dev/null
+++ b/test/GHC/Magic/Dict/Goods.hs
@@ -0,0 +1,37 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeApplications #-}
+{-# OPTIONS_GHC -dcore-lint -fobject-code #-}
+{-# OPTIONS_GHC -fplugin GHC.Magic.Dict.Plugin #-}
+
+module GHC.Magic.Dict.Goods (
+  eq2MyEqInt,
+  neq2MyEqInt,
+  eq2MyEqPoly,
+  neq2MyEqPoly,
+  unRelatedBy,
+  give,
+) where
+
+import GHC.Magic.Dict.Compat
+import GHC.Magic.Dict.Defs
+
+eq2MyEqInt :: Int -> Int -> Bool
+eq2MyEqInt = withDict @(MyEq Int) ((==) @Int) eq
+
+neq2MyEqInt :: Int -> Int -> Bool
+neq2MyEqInt = withDict @(MyEq Int) ((/=) @Int) eq
+
+eq2MyEqPoly :: forall a. (Eq a) => a -> a -> Bool
+eq2MyEqPoly = withDict @(MyEq a) ((==) @a) eq
+
+neq2MyEqPoly :: forall a. (Eq a) => a -> a -> Bool
+neq2MyEqPoly = withDict @(MyEq a) ((/=) @a) eq
+
+unRelatedBy :: forall a b. (a -> b -> Bool) -> a -> b -> Bool
+unRelatedBy rel = withDict @(Related a b) (fmap not . rel) related
+
+give :: forall a r. a -> ((Given a) => r) -> r
+give = withDict @(Given a)
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,1 @@
+{-# OPTIONS_GHC -F -pgmF tasty-discover -optF --tree-display #-}