diff --git a/CHANGELOG.md b/CHANGELOG.md
new file mode 100644
--- /dev/null
+++ b/CHANGELOG.md
@@ -0,0 +1,8 @@
+# 0.1.0.0 (2017-05-01)
+
+* Initial release. Everything is still rather experimental.
+  Feedback on any aspect of the library is welcome.
+
+  Currently, the general utilities are in
+  `Generics.SOP.Record`, and the subtyping functionality is
+  in `Generics.SOP.Record.SubTyping`.
diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,27 @@
+Copyright (c) 2017, Andres Löh
+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.
+
+3. Neither the name of the copyright holder nor the names of its 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 HOLDER 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/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/records-sop.cabal b/records-sop.cabal
new file mode 100644
--- /dev/null
+++ b/records-sop.cabal
@@ -0,0 +1,58 @@
+name: records-sop
+version: 0.1.0.0
+author: Andres Löh <andres@well-typed.com>
+maintainer: andres@well-typed.com
+license: BSD3
+license-file: LICENSE
+cabal-version: >= 1.10
+build-type: Simple
+tested-with: GHC == 8.0.1, GHC == 8.0.2, GHC == 8.2.1, GHC == 8.3.*
+category: Generics
+synopsis: Record subtyping and record utilities with generics-sop
+description:
+  This library provides utilities for working with labelled
+  single-constructor record types via generics-sop.
+  .
+  It also provides functions to safely cast between record
+  types if the target type has a subset of the fields (with
+  the same names) of the source type.
+extra-source-files: CHANGELOG.md
+
+source-repository head
+  type: git
+  location: https://github.com/kosmikus/records-sop
+
+library
+  hs-source-dirs:
+    src
+  ghc-options:
+    -Wall
+  exposed-modules:
+    Generics.SOP.Record,
+    Generics.SOP.Record.SubTyping
+  build-depends:
+    base >= 4.9 && < 5.0,
+    deepseq >= 1.3 && < 1.5,            
+    generics-sop >= 0.3 && < 0.4,
+    ghc-prim >= 0.5 && < 0.6
+  default-language:
+    Haskell2010
+
+test-suite examples
+  type:
+    exitcode-stdio-1.0
+  hs-source-dirs:
+    tests
+  ghc-options:
+    -Wall
+  main-is:
+    Examples.hs
+  build-depends:
+    base >= 4.9 && < 5.0,
+    deepseq >= 1.4 && < 1.5,
+    hspec >= 2.2 && < 2.5,
+    generics-sop >= 0.3 && < 0.4,
+    records-sop,
+    should-not-typecheck >= 2.1 && < 2.2
+  default-language:
+    Haskell2010
diff --git a/src/Generics/SOP/Record.hs b/src/Generics/SOP/Record.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/SOP/Record.hs
@@ -0,0 +1,275 @@
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE ConstraintKinds #-}
+{-# LANGUAGE DeriveGeneric #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE TypeInType #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE TypeOperators #-}
+{-# LANGUAGE UndecidableInstances #-}
+{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
+{-# OPTIONS_GHC -fno-warn-redundant-constraints #-}
+module Generics.SOP.Record
+  ( -- * A suitable representation for single-constructor records
+    FieldLabel
+  , RecordCode
+  , Record
+  , RecordRep
+    -- * Computing the record code
+  , RecordCodeOf
+  , IsRecord
+  , ValidRecordCode
+  , ExtractTypesFromRecordCode
+  , ExtractLabelsFromRecordCode
+  , RecombineRecordCode
+    -- * Conversion between a type and its record representation.
+  , toRecord
+  , fromRecord
+    -- * Utilities
+  , P(..)
+  , Snd
+  )
+  where
+
+import Control.DeepSeq
+import Generics.SOP.BasicFunctors
+import Generics.SOP.NP
+import Generics.SOP.NS
+import Generics.SOP.Universe
+import Generics.SOP.Sing
+import Generics.SOP.Type.Metadata
+import qualified GHC.Generics as GHC
+import GHC.TypeLits
+import GHC.Types
+import Unsafe.Coerce
+
+--------------------------------------------------------------------------
+-- A suitable representation for single-constructor records.
+--------------------------------------------------------------------------
+
+-- | On the type-level, we represent fiel labels using symbols.
+type FieldLabel = Symbol
+
+-- | The record code deviates from the normal SOP code in two
+-- ways:
+--
+-- - There is only one list, because we require that there is
+--   only a single constructor.
+--
+-- - In addition to the types of the fields, we store the labels
+--   of the fields.
+--
+type RecordCode = [(FieldLabel, Type)]
+
+-- | The record representation of a type is a record indexed
+-- by the record code.
+--
+type RecordRep (a :: Type) = Record (RecordCodeOf a)
+
+-- | The representation of a record is just a product indexed by
+-- a record code, containing elements of the types indicated
+-- by the code.
+--
+-- Note that the representation is deliberately chosen such that
+-- it has the same run-time representation as the product part
+-- of the normal SOP representation.
+--
+type Record (r :: RecordCode) = NP P r
+
+--------------------------------------------------------------------------
+-- Computing the record code
+--------------------------------------------------------------------------
+
+-- | This type-level function takes the type-level metadata provided
+-- by generics-sop as well as the normal generics-sop code, and transforms
+-- them into the record code.
+--
+-- Arguably, the record code is more usable than the representation
+-- directly on offer by generics-sop. So it's worth asking whether
+-- this representation should be included in generics-sop ...
+--
+-- The function will only reduce if the argument type actually is a
+-- record, meaning it must have exactly one constructor, and that
+-- constructor must have field labels attached to it.
+--
+type RecordCodeOf a = ToRecordCode_Datatype a (DatatypeInfoOf a) (Code a)
+
+-- | Helper for 'RecordCodeOf', handling the datatype level. Both
+-- datatypes and newtypes are acceptable. Newtypes are just handled
+-- as one-constructor datatypes for this purpose.
+--
+type family
+  ToRecordCode_Datatype (a :: Type) (d :: DatatypeInfo) (c :: [[Type]]) :: RecordCode where
+  ToRecordCode_Datatype a (ADT _ _ cis)    c = ToRecordCode_Constructor a cis c
+  ToRecordCode_Datatype a (Newtype _ _ ci) c = ToRecordCode_Constructor a '[ ci ] c
+
+-- | Helper for 'RecordCodeOf', handling the constructor level. Only
+-- single-constructor types are acceptable, and the constructor must
+-- contain field labels.
+--
+-- As an exception, we accept an empty record, even though it does
+-- not explicitly define any field labels.
+--
+type family
+  ToRecordCode_Constructor (a :: Type) (cis :: [ConstructorInfo]) (c :: [[Type]]) :: RecordCode where
+  ToRecordCode_Constructor a '[ 'Record _ fis  ] '[ ts  ] = ToRecordCode_Field fis ts
+  ToRecordCode_Constructor a '[ 'Constructor _ ] '[ '[] ] = '[]
+  ToRecordCode_Constructor a '[]                  _       =
+    TypeError
+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
+      :$$: Text "It has no constructors."
+      )
+  ToRecordCode_Constructor a ( _ : _ : _ )        _       =
+    TypeError
+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
+      :$$: Text "It has more than one constructor."
+      )
+  ToRecordCode_Constructor a '[ _ ]               _       =
+    TypeError
+      (    Text "The type `" :<>: ShowType a :<>: Text "' is not a record type."
+      :$$: Text "It has no labelled fields."
+      )
+
+-- | Helper for 'RecordCodeOf', handling the field level. At this point,
+-- we simply zip the list of field names and the list of types.
+--
+type family ToRecordCode_Field (fis :: [FieldInfo]) (c :: [Type]) :: RecordCode where
+  ToRecordCode_Field '[]                    '[]        = '[]
+  ToRecordCode_Field ( 'FieldInfo l : fis ) ( t : ts ) = '(l, t) : ToRecordCode_Field fis ts
+
+-- * Relating the record code and the original code.
+
+-- | The constraint @IsRecord a r@ states that the type 'a' is a record type
+-- (i.e., has exactly one constructor and field labels) and that 'r' is the
+-- record code associated with 'a'.
+--
+type IsRecord (a :: Type) (r :: RecordCode) =
+  IsRecord' a r (GetSingleton (Code a))
+
+-- | The constraint @IsRecord' a r xs@ states that 'a' is a record type
+-- with record code 'r', and that the types contained in 'r' correspond
+-- to the list 'xs'.
+--
+-- If the record code computation is correct, then the record code of a
+-- type is strongly related to the original generics-sop code. Extracting
+-- the types out of 'r' should correspond to 'xs'. Recombining the
+-- labels from 'r' with 'xs' should yield 'r' exactly. These sanity
+-- properties are captured by 'ValidRecordCode'.
+--
+type IsRecord' (a :: Type) (r :: RecordCode) (xs :: [Type]) =
+  ( Generic a, Code a ~ '[ xs ]
+  , RecordCodeOf a ~ r, ValidRecordCode r xs
+  )
+
+-- | Relates a recordcode 'r' and a list of types 'xs', stating that
+-- 'xs' is indeed the list of types contained in 'r'.
+--
+type ValidRecordCode (r :: RecordCode) (xs :: [Type]) =
+  ( ExtractTypesFromRecordCode r ~ xs
+  , RecombineRecordCode (ExtractLabelsFromRecordCode r) xs ~ r
+  )
+
+-- | Extracts all the types from a record code.
+type family ExtractTypesFromRecordCode (r :: RecordCode) :: [Type] where
+  ExtractTypesFromRecordCode '[]             = '[]
+  ExtractTypesFromRecordCode ( '(_, a) : r ) = a : ExtractTypesFromRecordCode r
+
+-- | Extracts all the field labels from a record code.
+type family ExtractLabelsFromRecordCode (r :: RecordCode) :: [FieldLabel] where
+  ExtractLabelsFromRecordCode '[]             = '[]
+  ExtractLabelsFromRecordCode ( '(l, _) : r ) = l : ExtractLabelsFromRecordCode r
+
+-- | Given a list of labels and types, recombines them into a record code.
+--
+-- An important aspect of this function is that it is defined by induction
+-- on the list of types, and forces the list of field labels to be at least
+-- as long.
+--
+type family RecombineRecordCode (ls :: [FieldLabel]) (ts :: [Type]) :: RecordCode where
+  RecombineRecordCode _ '[]       = '[]
+  RecombineRecordCode ls (t : ts) = '(Head ls, t) : RecombineRecordCode (Tail ls) ts
+
+--------------------------------------------------------------------------
+-- Conversion between a type and its record representation.
+--------------------------------------------------------------------------
+
+-- | Convert a value into its record representation.
+toRecord :: (IsRecord a _r) => a -> RecordRep a
+toRecord = unsafeToRecord_NP . unZ . unSOP . from
+
+-- | Convert an n-ary product into the corresponding record
+-- representation. This is a no-op, and more efficiently
+-- implented using 'unsafeToRecord_NP'. It is included here
+-- to demonstrate that it actually is type-correct and also
+-- to make it more obvious that it is indeed a no-op.
+--
+_toRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
+_toRecord_NP Nil         = Nil
+_toRecord_NP (I x :* xs) = P x :* _toRecord_NP xs
+
+-- | Fast version of 'toRecord_NP'. Not actually unsafe as
+-- long as the internal representations of 'NP' and 'Record'
+-- are not changed.
+--
+unsafeToRecord_NP :: (ValidRecordCode r xs) => NP I xs -> Record r
+unsafeToRecord_NP = unsafeCoerce
+
+-- | Convert a record representation back into a value.
+fromRecord :: (IsRecord a r) => RecordRep a -> a
+fromRecord = to . SOP . Z . unsafeFromRecord_NP
+
+-- | Convert a record representation into an n-ary product. This is a no-op,
+-- and more efficiently implemented using 'unsafeFromRecord_NP'.
+--
+-- It is also noteworthy that we let the resulting list drive the computation.
+-- This is compatible with the definition of 'RecombineRecordCode' based on
+-- the list of types.
+--
+_fromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
+_fromRecord_NP = case sList :: SList xs of
+  SNil  -> const Nil
+  SCons -> \ r -> case r of
+    P x :* xs -> I x :* _fromRecord_NP xs
+
+-- | Fast version of 'fromRecord_NP'. Not actually unsafe as
+-- long as the internal representation of 'NP' and 'Record'
+-- are not changed.
+--
+unsafeFromRecord_NP :: forall r xs . (ValidRecordCode r xs, SListI xs) => Record r -> NP I xs
+unsafeFromRecord_NP = unsafeCoerce
+
+--------------------------------------------------------------------------
+-- Utilities
+--------------------------------------------------------------------------
+ 
+-- | Projection of the second component of a type-level pair,
+-- wrapped in a newtype.
+--
+newtype P (p :: (a, Type)) = P (Snd p)
+  deriving (GHC.Generic)
+
+deriving instance Eq a => Eq (P '(l, a))
+deriving instance Ord a => Ord (P '(l, a))
+deriving instance Show a => Show (P '(l, a))
+
+instance NFData a => NFData (P '(l, a)) where
+  rnf (P x) = rnf x
+
+-- | Type-level variant of 'snd'.
+type family Snd (p :: (a, b)) :: b where
+  Snd '(a, b) = b
+
+-- | Type-level variant of 'head'.
+type family Head (xs :: [k]) :: k where
+  Head (x : xs) = x
+
+-- | Type-level variant of 'tail'.
+type family Tail (xs :: [k]) :: [k] where
+  Tail (x : xs) = xs
+
+-- | Partial type-level function that extracts the only element
+-- from a singleton type-level list.
+--
+type family GetSingleton (xs :: [k]) :: k where
+  GetSingleton '[ x ] = x
diff --git a/src/Generics/SOP/Record/SubTyping.hs b/src/Generics/SOP/Record/SubTyping.hs
new file mode 100644
--- /dev/null
+++ b/src/Generics/SOP/Record/SubTyping.hs
@@ -0,0 +1,87 @@
+{-# LANGUAGE
+    AllowAmbiguousTypes
+  , FlexibleInstances
+  , MultiParamTypeClasses
+  , ScopedTypeVariables
+  , TypeApplications
+  , TypeInType
+  , TypeFamilies
+  , TypeOperators
+  , UndecidableInstances
+#-}
+{-# OPTIONS_GHC
+  -fno-warn-unticked-promoted-constructors
+#-}
+module Generics.SOP.Record.SubTyping
+  ( cast
+  , IsSubTypeOf
+  , IsElemOf
+  )
+  where
+
+import Data.Type.Equality
+import Generics.SOP.NP
+import GHC.Types
+
+import Generics.SOP.Record
+
+-- | Cast one record type to another if there is a subtype relationship
+-- between them. Currently, only width subtyping is considered, which means
+-- that we can forget and reorder fields.
+--
+cast :: (IsRecord a ra, IsRecord b rb, IsSubTypeOf ra rb) => a -> b
+cast = fromRecord . castRecord . toRecord
+
+-- | Class that checks whether one record code is convertible into another.
+--
+-- Conversion works if the first record contains at least the labels of the
+-- second record, and if the types of the corresponding fields match exactly.
+--
+class IsSubTypeOf (r1 :: RecordCode) (r2 :: RecordCode) where
+  -- | Perform a safe cast between two records.
+  castRecord :: Record r1 -> Record r2
+
+instance IsSubTypeOf r1 '[] where
+  castRecord _ = Nil
+
+instance (IsSubTypeOf r1 r2, IsElemOf s2 a2 r1) => IsSubTypeOf r1 ( '(s2, a2) : r2 ) where
+  castRecord r = P (get @s2 r) :* castRecord r
+
+-- | Class that checks whether a field of a particular type is contained
+-- in a record.
+--
+class IsElemOf (s :: Symbol) (a :: Type) (r :: RecordCode) where
+  -- | Perform an extraction of a given field. Field name has to be passed
+  -- via type application.
+  --
+  get :: Record r -> a
+
+-- | Helper class. Isn't strictly needed, but allows us to avoid
+-- overlapping instances for the 'IsElemOf' class.
+--
+class IsElemOf' (b :: Bool)
+  (s1 :: FieldLabel) (a1 :: Type)
+  (s2 :: FieldLabel) (a2 :: Type)
+  (r :: RecordCode)
+  where
+  get' :: Record ( '(s2, a2) : r ) -> a1
+
+instance
+  IsElemOf' (SameFieldLabel s1 s2) s1 a1 s2 a2 r =>
+  IsElemOf s1 a1 ( '(s2, a2) : r )
+  where
+  get = get' @(SameFieldLabel s1 s2) @s1
+
+instance (a1 ~ a2) => IsElemOf' True s a1 s a2 r where
+  get' (P a :* _) = a
+
+instance IsElemOf s1 a1 r => IsElemOf' False s1 a1 s2 a2 r where
+  get' (_ :* r) = get @s1 r
+
+-- | Decide the equality of two field labels.
+--
+-- Just a special case of polymorphic type equality.
+--
+type family
+  SameFieldLabel (s1 :: FieldLabel) (s2 :: FieldLabel) :: Bool where
+  SameFieldLabel s1 s2 = s1 == s2
diff --git a/tests/Examples.hs b/tests/Examples.hs
new file mode 100644
--- /dev/null
+++ b/tests/Examples.hs
@@ -0,0 +1,172 @@
+{-# LANGUAGE
+    DeriveGeneric
+  , DuplicateRecordFields
+#-}
+{-# OPTIONS_GHC -fdefer-type-errors -Wno-deferred-type-errors #-}
+module Main where
+
+import Control.DeepSeq
+import qualified GHC.Generics as GHC
+import Test.Hspec
+import Test.ShouldNotTypecheck
+
+import Generics.SOP
+import Generics.SOP.Record
+import Generics.SOP.Record.SubTyping
+
+data X = MkX {}
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic X
+instance HasDatatypeInfo X
+instance NFData X
+
+data A = MkA { anInt :: Int, aBool :: Bool }
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic A
+instance HasDatatypeInfo A
+instance NFData A
+
+data B = MkB { anInt :: Int, aBool :: Bool, aChar :: Char }
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic B
+instance HasDatatypeInfo B
+instance NFData B
+
+-- Permutation.
+data C = MkC { aBool :: Bool, aChar :: Char, anInt :: Int }
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic C
+instance HasDatatypeInfo C
+instance NFData C
+
+-- Duplicate label within a single record (works!).
+data D = MkD { anInt :: Int, anInt :: Int }
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic D
+instance HasDatatypeInfo D
+instance NFData D
+
+-- Wrong type.
+data E = MkE { anInt :: Int, aBool :: Bool, aChar :: () }
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic E
+instance HasDatatypeInfo E
+instance NFData E
+
+-- No field labels.
+data F = MkF Int Bool Char
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic F
+instance HasDatatypeInfo F
+instance NFData F
+
+-- Two constructors.
+data G = MkG { anInt :: Int, aBool :: Bool, aChar :: Char }
+       | OtherG
+  deriving (Eq, Show, GHC.Generic)
+
+instance Generic G
+instance HasDatatypeInfo G
+instance NFData G
+
+a :: A
+a = MkA 3 True
+
+b :: B
+b = MkB 3 True 'x'
+
+c :: C
+c = MkC True 'x' 3
+
+d :: D
+d = MkD 3 3
+
+d' :: D
+d' = MkD 3 4
+
+e :: E
+e = MkE 3 True ()
+
+f :: F
+f = MkF 3 True 'x'
+
+g :: G
+g = MkG 3 True 'x'
+
+x :: X
+x = MkX {}
+
+main :: IO ()
+main = hspec $
+  describe "cast" $ do
+    it "successfully casts X to X" $
+      (cast x :: X) `shouldBe` x
+    it "successfully casts A to A" $
+      (cast a :: A) `shouldBe` a
+    it "successfully casts A to X" $
+      (cast a :: X) `shouldBe` x
+    it "successfully casts A to D" $
+      (cast a :: D) `shouldBe` d
+    it "successfully casts B to B" $
+      (cast b :: B) `shouldBe` b
+    it "successfully casts B to X" $
+      (cast b :: X) `shouldBe` x
+    it "successfully casts B to A" $
+      (cast b :: A) `shouldBe` a
+    it "successfully casts B to C" $
+      (cast b :: C) `shouldBe` c
+    it "successfully casts B to D" $
+      (cast b :: D) `shouldBe` d
+    it "successfully casts C to X" $
+      (cast c :: X) `shouldBe` x
+    it "successfully casts C to A" $
+      (cast c :: A) `shouldBe` a
+    it "successfully casts C to B" $
+      (cast c :: B) `shouldBe` b
+    it "successfully casts C to D" $
+      (cast c :: D) `shouldBe` d
+    it "successfully casts D to D" $
+      (cast d :: D) `shouldBe` d
+    it "prefers the first element when casting D to D" $
+      (cast d' :: D) `shouldBe` d
+    it "successfully casts D to X" $
+      (cast d :: X) `shouldBe` x
+    it "successfully casts E to E" $
+      (cast e :: E) `shouldBe` e
+    it "successfully casts E to X" $
+      (cast e :: X) `shouldBe` x
+    it "successfully casts E to A" $
+      (cast e :: A) `shouldBe` a
+    it "successfully casts E to D" $
+      (cast e :: D) `shouldBe` d
+    it "correctly fails to cast A to B" $
+      shouldNotTypecheck (cast a :: B)
+    it "correctly fails to cast A to C" $
+      shouldNotTypecheck (cast a :: C)
+    it "correctly fails to cast D to A" $
+      shouldNotTypecheck (cast d :: A)
+    it "correctly fails to cast D to B" $
+      shouldNotTypecheck (cast d :: B)
+    it "correctly fails to cast D to C" $
+      shouldNotTypecheck (cast d :: C)
+    it "correctly fails to cast E to B" $
+      shouldNotTypecheck (cast e :: B)
+    it "correctly fails to cast E to C" $
+      shouldNotTypecheck (cast e :: C)
+    -- The following two produce type errors as expected.
+    -- Unfortunately, user-defined type errors in combination
+    -- with shouldNotTypeCheck seems to trigger an internal
+    -- error ... (see GHC bug #12104)
+{-
+    it "fails to cast F to anything (even X)" $
+      shouldNotTypecheck (cast f :: X)
+    it "fails to cast G to anything (even X)" $
+      shouldNotTypecheck (cast g :: X)
+-}