summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorsjakobi <>2019-09-10 12:35:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2019-09-10 12:35:00 (GMT)
commit01fedd090c668b32f66132018b476e09db1f3701 (patch)
tree4f31061aa6498699feb6adf22cab10fe2e0a1bd4
parent484a2d64edfc3415372d3d7a6e2998c3d8cc7c20 (diff)
version 0.1.0HEAD0.1.0master
-rw-r--r--CHANGELOG.md14
-rw-r--r--Setup.hs2
-rw-r--r--coercible-utils.cabal17
-rw-r--r--src/CoercibleUtils.hs200
-rw-r--r--src/CoercibleUtils/Compose.hs51
-rw-r--r--src/CoercibleUtils/Newtype.hs328
-rw-r--r--test/Spec.hs103
7 files changed, 517 insertions, 198 deletions
diff --git a/CHANGELOG.md b/CHANGELOG.md
index dd2ac91..8fe4913 100644
--- a/CHANGELOG.md
+++ b/CHANGELOG.md
@@ -1,12 +1,24 @@
# Changelog
`coercible-utils` uses [PVP Versioning][PVP].
+## [0.1.0] – 2019-09-07
+
+* Improve type inference via a new generic `Newtype` class. ([#14], [#16])
+* Improve type signatures to point out which arguments are used only to
+ direct type inference. ([#13])
+
+
## [0.0.0] – 2018-06-29
Initial release.
-[Unreleased]: https://github.com/sjakobi/coercible-utils/compare/v0.0.0...HEAD
+[Unreleased]: https://github.com/sjakobi/coercible-utils/compare/v0.1.0...HEAD
+[0.1.0]: https://github.com/sjakobi/coercible-utils/compare/v0.0.0...v0.1.0
[0.0.0]: https://github.com/sjakobi/coercible-utils/releases/tag/v0.0.0
+[#13]: https://github.com/sjakobi/coercible-utils/pull/13
+[#14]: https://github.com/sjakobi/coercible-utils/pull/14
+[#16]: https://github.com/sjakobi/coercible-utils/pull/16
+
[PVP]: https://pvp.haskell.org
diff --git a/Setup.hs b/Setup.hs
deleted file mode 100644
index 9a994af..0000000
--- a/Setup.hs
+++ /dev/null
@@ -1,2 +0,0 @@
-import Distribution.Simple
-main = defaultMain
diff --git a/coercible-utils.cabal b/coercible-utils.cabal
index 2db934c..086824d 100644
--- a/coercible-utils.cabal
+++ b/coercible-utils.cabal
@@ -1,29 +1,30 @@
name: coercible-utils
-version: 0.0.0
+version: 0.1.0
description: Utility functions for Coercible types.
-synopsis: Utility functions for Coercible types.
+synopsis: Utility functions for Coercible types
homepage: https://github.com/sjakobi/coercible-utils
bug-reports: https://github.com/sjakobi/coercible-utils/issues
license: BSD3
license-file: LICENSE
-author: Simon Jakobi, chessai
+author: Simon Jakobi, chessai, David Feuer
maintainer: simon.jakobi@gmail.com
copyright: 2018 Simon Jakobi, chessai
category: Control
build-type: Simple
extra-doc-files: CHANGELOG.md
cabal-version: 1.24
-tested-with: GHC == 7.10.3
- , GHC == 8.0.2
- , GHC == 8.2.2
- , GHC == 8.4.3
+tested-with: GHC == 8.4.4
+ , GHC == 8.6.5
+ , GHC == 8.8.1
library
hs-source-dirs: src
exposed-modules: CoercibleUtils
+ , CoercibleUtils.Compose
+ , CoercibleUtils.Newtype
ghc-options: -Wall
- build-depends: base >= 4.8 && < 4.13
+ build-depends: base >= 4.11 && < 4.14
default-language: Haskell2010
diff --git a/src/CoercibleUtils.hs b/src/CoercibleUtils.hs
index 616ddb3..fa422e7 100644
--- a/src/CoercibleUtils.hs
+++ b/src/CoercibleUtils.hs
@@ -1,194 +1,22 @@
-{- |
-Primarily pulled from the
-package @[newtype-generics](http://hackage.haskell.org/package/newtype-generics)@,
-and based on Conor McBride's Epigram work, but
-generalised to work over anything `Coercible`.
-
->>> ala Sum foldMap [1,2,3,4 :: Int] :: Int
-10
+{-# language TypeOperators #-}
->>> ala Endo foldMap [(+1), (+2), (subtract 1), (*2) :: Int -> Int] (3 :: Int) :: Int
-8
-
->>> under2 Min (<>) 2 (1 :: Int) :: Int
-1
+{- |
+This module reexports the entire content of the `coercible-utils` package.
->>> over All not (All False) :: All
-All {getAll = True)
+See the 'CoercibleUtils.Newtype' module for the newtype combinators.
-__Note__: All of the functions in this module take an argument that solely
+__Note__: Most functions in this package take an argument that solely
directs the /type/ of the coercion. The value of this argument is /ignored/.
+In each case, this argument has a type that looks like @a \`to\` b@. As the name
+of the @to@ type variable suggests, this will typically be a function from
+@a@ to @b@. But leaving the type variable completely polymorphic and
+unconstrained lets the type signature communicate the fact that the argument
+is not used.
-}
module CoercibleUtils
- ( -- * Coercive composition
- (#.), (.#)
-
- -- * The classic "newtype" combinators
- , op
- , ala, ala'
- , under, over
- , under2, over2
- , underF, overF
+ ( module CoercibleUtils.Newtype
+ , (#.), (.#)
) where
-import Data.Coerce (Coercible, coerce)
-
--- | Coercive left-composition.
---
--- >>> (All #. not) True
--- All {getAll = False}
---
--- The semantics with respect to bottoms are:
---
--- @
--- p '#.' ⊥ ≡ ⊥
--- p '#.' f ≡ p '.' f
--- @
-infixr 9 #.
-(#.) :: Coercible b c => (b -> c) -> (a -> b) -> a -> c
-(#.) _ = coerce
-{-# INLINE (#.) #-}
-
--- | Coercive right-composition.
---
--- >>> (stimes 2 .# Product) 3
--- Product {getProduct = 9}
---
--- The semantics with respect to bottoms are:
---
--- @
--- ⊥ '.#' p ≡ ⊥
--- f '.#' p ≡ p '.' f
--- @
-infixr 9 .#
-(.#) :: Coercible a b => (b -> c) -> (a -> b) -> a -> c
-(.#) f _ = coerce f
-{-# INLINE (.#) #-}
-
--- | Reverse the type of a "packer".
---
--- >>> op All (All True)
--- True
--- >>> op (Identity . Sum) (Identity (Sum 3))
--- 3
-op :: Coercible a b
- => (a -> b)
- -> b
- -> a
-op = coerce
-{-# INLINE op #-}
-
--- | The workhorse of the package. Given a "packer" and a \"higher order function\" (/hof/),
--- it handles the packing and unpacking, and just sends you back a regular old
--- function, with the type varying based on the /hof/ you passed.
---
--- The reason for the signature of the /hof/ is due to 'ala' not caring about structure.
--- To illustrate why this is important, consider this alternative implementation of 'under2':
---
--- @
--- under2' :: (Coercible a b, Coercible a' b')
--- => (a -> b) -> (b -> b -> b') -> (a -> a -> a')
--- under2' pa f o1 o2 = 'ala' pa (\\p -> uncurry f . bimap p p) (o1, o2)
--- @
---
--- Being handed the "packer", the /hof/ may apply it in any structure of its choosing –
--- in this case a tuple.
---
--- >>> ala Sum foldMap [1,2,3,4 :: Int] :: Int
--- 10
-ala :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> ((a -> b) -> c -> b')
- -> c
- -> a'
-ala pa hof = ala' pa hof id
-{-# INLINE ala #-}
-
--- | The way it differs from the 'ala' function in this package,
--- is that it provides an extra hook into the \"packer\" passed to the hof.
---
--- However, this normally ends up being 'id', so 'ala' wraps this function and
--- passes 'id' as the final parameter by default.
--- If you want the convenience of being able to hook right into the /hof/,
--- you may use this function.
---
--- >>> ala' Sum foldMap length ["hello", "world"] :: Int
--- 10
---
--- >>> ala' First foldMap (readMaybe @Int) ["x", "42", "1"] :: Maybe Int
--- Just 42
-ala' :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> ((d -> b) -> c -> b')
- -> (d -> a)
- -> c
- -> a'
-ala' _ hof f = coerce #. hof (coerce f)
-{-# INLINE ala' #-}
-
--- | A very simple operation involving running the function /under/ the "packer".
---
--- >>> under Product (stimes 3) (3 :: Int) :: Int
--- 27
-under :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> (b -> b')
- -> a
- -> a'
-under _ f = coerce f
-{-# INLINE under #-}
-
--- | The opposite of 'under'. I.e., take a function which works on the
--- underlying "unpacked" types, and switch it to a function that works
--- on the "packer".
---
--- >>> over All not (All False) :: All
--- All {getAll = True}
-over :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> (a -> a')
- -> b
- -> b'
-over _ f = coerce f
-{-# INLINE over #-}
-
--- | Lower a binary function to operate on the underlying values.
---
--- >>> under2 Any (<>) True False :: Bool
--- True
-under2 :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> (b -> b -> b')
- -> a
- -> a
- -> a'
-under2 _ f = coerce f
-{-# INLINE under2 #-}
-
--- | The opposite of 'under2'.
-over2 :: (Coercible a b, Coercible a' b')
- => (a -> b)
- -> (a -> a -> a')
- -> b
- -> b
- -> b'
-over2 _ f = coerce f
-{-# INLINE over2 #-}
-
--- | 'under' lifted into a 'Functor'.
-underF :: (Coercible a b, Coercible a' b', Functor f, Functor g)
- => (a -> b)
- -> (f b -> g b')
- -> f a
- -> g a'
-underF _ f = fmap coerce . f . fmap coerce
-{-# INLINE underF #-}
-
--- | 'over' lifted into a 'Functor'.
-overF :: (Coercible a b, Coercible a' b', Functor f, Functor g)
- => (a -> b)
- -> (f a -> g a')
- -> f b
- -> g b'
-overF _ f = fmap coerce . f . fmap coerce
-{-# INLINE overF #-}
+import CoercibleUtils.Compose ((#.), (.#))
+import CoercibleUtils.Newtype
diff --git a/src/CoercibleUtils/Compose.hs b/src/CoercibleUtils/Compose.hs
new file mode 100644
index 0000000..e6c205c
--- /dev/null
+++ b/src/CoercibleUtils/Compose.hs
@@ -0,0 +1,51 @@
+{-# language TypeOperators #-}
+
+{-|
+Coercive function composition.
+
+__Note__: The functions in this module take an argument that solely
+directs the /type/ of the coercion. The value of this argument is /ignored/.
+In each case, this argument has a type that looks like @a \`to\` b@. As the name
+of the @to@ type variable suggests, this will typically be a function from
+@a@ to @b@. But leaving the type variable completely polymorphic and
+unconstrained lets the type signature communicate the fact that the argument
+is not used.
+-}
+module CoercibleUtils.Compose
+ ( (#.)
+ , (.#)
+ ) where
+
+import Data.Coerce (Coercible, coerce)
+
+-- | Coercive left-composition.
+--
+-- >>> (All #. not) True
+-- All {getAll = False}
+--
+-- The semantics with respect to bottoms are:
+--
+-- @
+-- p '#.' ⊥ ≡ ⊥
+-- p '#.' f ≡ p '.' f
+-- @
+infixr 9 #.
+(#.) :: Coercible b c => (b `to` c) -> (a -> b) -> a -> c
+(#.) _ = coerce
+{-# INLINE (#.) #-}
+
+-- | Coercive right-composition.
+--
+-- >>> (stimes 2 .# Product) 3
+-- Product {getProduct = 9}
+--
+-- The semantics with respect to bottoms are:
+--
+-- @
+-- ⊥ '.#' p ≡ ⊥
+-- f '.#' p ≡ p '.' f
+-- @
+infixr 9 .#
+(.#) :: Coercible a b => (b -> c) -> (a `to` b) -> a -> c
+(.#) f _ = coerce f
+{-# INLINE (.#) #-}
diff --git a/src/CoercibleUtils/Newtype.hs b/src/CoercibleUtils/Newtype.hs
new file mode 100644
index 0000000..ee2e1f7
--- /dev/null
+++ b/src/CoercibleUtils/Newtype.hs
@@ -0,0 +1,328 @@
+{-# language FlexibleContexts #-}
+{-# language FlexibleInstances #-}
+{-# language MultiParamTypeClasses #-}
+{-# language ScopedTypeVariables #-}
+{-# language TypeFamilies #-}
+{-# language TypeOperators #-}
+{-# language DataKinds #-}
+{-# language UndecidableInstances #-}
+{-# language ConstraintKinds #-}
+{-# language PolyKinds #-}
+
+{- |
+A version of the 'Newtype' typeclass and related functions. The API is
+primarily pulled from Conor McBride's Epigram work. The general idea is that we
+can manipulate types in terms of newtypes around them or newtypes in terms of
+their underlying types. Some examples:
+
+>>> ala Sum foldMap [1,2,3,4]
+10
+
+>>> ala Endo foldMap [(+1), (+2), (subtract 1), (*2)] 3
+8
+
+>>> under2 Min (<>) 2 1
+1
+
+>>> over All not (All False)
+All {getAll = True)
+
+The version of the 'Newtype' class exported by this module has an instance for
+*all* and *only* newtypes with 'Generic' instances whose generated
+'Coercible' instances are visible. Users need not, and probably should not, write
+their own instances.
+
+Like McBride's version, and unlike the one in @newtype-generics@, this version
+has two parameters: one for the newtype and one for the underlying type. This
+is mostly a matter of taste.
+
+__Note__: Most functions in this module take an argument representing a newtype
+constructor. This is used only for its type. To make that clear, the type of
+that argument is allowed to be extremely polymorphic: @o \`to\` n@ rather than
+@o -> n@. Unfortunately, GHCi displays this as @to o n@, which is ugly but
+equivalent.
+
+General approach: When the type variables @n@ and @o@ appear, @n@ is required
+to be a newtype wrapper around @o@. Similarly, when the type variables @n'@ and
+@o'@ appear as well, @n'@ is required to be a newtype wrapper around @o'@.
+Furthermore, in this case, @n@ and @n'@ are required to be the /same newtype/,
+with possibly different type arguments. See 'Similar' for detailed
+documentation.
+
+@since TODO
+-}
+module CoercibleUtils.Newtype
+ ( Newtype
+ , IsNewtype
+ , HasUnderlying
+ , O
+ , Similar
+ , pack
+ , unpack
+ , op
+ , ala
+ , ala'
+ , under
+ , over
+ , under2
+ , over2
+ , underF
+ , overF
+ ) where
+
+import GHC.Generics
+import Data.Coerce
+import GHC.TypeLits (TypeError, ErrorMessage (..))
+import CoercibleUtils.Compose ((#.), (.#))
+import Data.Kind (Constraint)
+
+-- | Get the underlying type of a newtype.
+--
+-- @
+-- data N = N Int deriving Generic
+-- -- O N = Int
+-- @
+type O x = GO (Rep x)
+
+-- | Get the underlying type of a newtype from its generic
+-- representation.
+type family GO rep where
+ GO (D1 _d (C1 _c (S1 _s (K1 _i a)))) = a
+
+-- | Given types @x@ and @o@, produce a constraint requiring that @x@ be a
+-- newtype whose underlying type is @o@.
+type NewtypeF x o = GNewtypeF x (Rep x) o
+
+-- | Putting a newtype check and 'TypeError' call in 'GO' and then requiring @o
+-- ~ O n@ doesn't get us a custom type error when we want one. Calculating the
+-- constraint with an error case, however, seems to do the trick.
+type family GNewtypeF x rep o :: Constraint where
+ GNewtypeF _x (D1 ('MetaData _n _m _p 'True) (C1 _c (S1 _s (K1 _i a)))) o = a ~ o
+ GNewtypeF x _rep _o = TypeError
+ ('Text "There is no " ':<>: 'ShowType Newtype ':<>: 'Text " instance for"
+ ':$$: 'Text " " ':<>: 'ShowType x
+ ':$$: 'Text "because it is not a newtype.")
+
+-- | @Newtype n o@ means that @n@ is a newtype wrapper around @o@. @n@ must be
+-- an instance of 'Generic'. Furthermore, the @'Coercible' n o@ instance must
+-- be visible; this typically means the newtype constructor is visible, but the
+-- instance could also have been brought into view by pattern matching on a
+-- 'Data.Type.Coercion.Coercion'.
+class Coercible n o => Newtype (n :: k) (o :: k)
+
+-- The Generic n constraint gives a much better type error if n is not an
+-- instance of Generic. Without that, there's just a mysterious message
+-- involving GO and Rep. With it, the lousy error message still shows up, but
+-- at least there's also a good one.
+instance (Generic n, NewtypeF n o, Coercible n o) => Newtype n o
+
+-- | A single-parameter version of 'Newtype', similar to the @Newtype@ class in
+-- @newtype-generics@.
+--
+-- @Newtype n o@ is equivalent to @(IsNewtype n, o ~ O n)@.
+class Newtype n (O n) => IsNewtype n
+instance Newtype n (O n) => IsNewtype n
+
+-- | A version of 'Newtype' with the parameters flipped, for partial
+-- application.
+class Newtype n o => HasUnderlying o n
+instance Newtype n o => HasUnderlying o n
+
+-- | Two types are @Similar@ if they are built from
+-- the same type constructor and the same kind arguments.
+--
+-- @Sum Int@ and @Sum Bool@ are @Similar@.
+--
+-- @Sum Int@ and @Product Int@ are not @Similar@
+-- because they are built from different type constructors.
+--
+-- @Const Int Char@ and @Const Int Maybe@ are not @Similar@
+-- because they have different kind arguments.
+class Similar (n :: k) (n' :: k)
+-- See [Note: Similar implementation]
+
+instance (Similar' n n', Similar' n' n) => Similar n n'
+
+-- | Given a type of the form (f b), try to extract b, assuming that b is of
+-- kind kb. Note that kb itself is an implicit argument to GetArg; the
+-- surrounding context of the call must determine kb.
+type family GetArg (x :: kx) :: kb where
+ GetArg (_ b) = b
+
+-- | Given a type of the form (f b), try to extract f, assuming that f is of
+-- kind kf. Note that kf itself is an implicit argument to GetFun; the
+-- surrounding context of the call must determine kf.
+type family GetFun (x :: kx) :: kf where
+ GetFun (f _) = f
+
+-- | Given types @n@ and @n'@, produce a constraint requiring that @n'@ be
+-- built from the same newtype constructor as @n@. See [Note: Similar
+-- implementation].
+type family Similar' (n :: k) (n' :: k) :: Constraint where
+ Similar' (f (_a :: ka)) n' =
+ ( Similar' f (GetFun n')
+ , n' ~ GetFun n' (GetArg n' :: ka))
+ Similar' f g = f ~ g
+-- We capture the kind of the argument as ka, and pass it to GetArg.
+-- The kind of the first call to GetFun is fixed by the kind of f,
+-- while the kind of the second is fixed by the kind of n' and the
+-- imposed kind, ka, of GetArg.
+
+{-
+[Note: Similar implementation]
+
+The Similar class is what really separates this implementation of this API from
+all previous ones of which I am aware. Since it's not the simplest thing, I'll
+give an extended description of the implementation here.
+
+We really want n to give us information about n'. It's also nice (for typed
+holes and error messages, particularly) if n' gives us information about n.
+Since we may know nothing, a priori, about one of those, we have to be a bit
+careful not to force a match on one when the other is the one with information.
+The horrible way to do that (even worse :t results!) is with INCOHERENT
+typeclass instances. Ignoring that awfulness, the thing to do is to require n'
+to have a structure calculated from n and the other way around, "in parallel".
+Similar' n n' matches on n, producing a constraint. Suppose we have n ~ F a b.
+Then we get
+
+ Similar' (F a b) n'
+ (Similar' (F a) (GetFun n'), n' ~ GetFun n' (GetArg n'))
+
+We have now constrained things only a little: n' is required to have the form p
+q for some p and q, where F a and p have the same kind and b and q have the
+same kind. Substituting in p and q, we continue:
+
+ (Similar' (F a) p, n' ~ p q)
+ ((Similar' F (GetFun p), p ~ GetFun p (GetArg p)), n' ~ p q)
+
+Let's set r ~ GetFun p and s ~ GetArg p. Then
+
+ ((Similar' F r, p ~ r s), n' ~ p q)
+
+We've now reached the base case! Yay! So the last step is
+
+ ((F ~ r, p ~ r s), n' ~ p q)
+
+which then simplifies to
+
+ n' ~ F s q
+
+Undoing the substitutions we made,
+
+ n' ~ F (GetArg (GetFun n')) (GetArg n')
+
+The arguments in that constraint are completely useless (as far as I know), but
+we need to put it all together like that to get what we're after: an equality
+constraint on n' itself that lets GHC know it's F x y for some x and y to be
+determined. Very often, those are then fixed by the type o' and the Newtype n'
+o' constraint, which at first seems backwards. Say we consider Sum. We have
+
+ type Rep (Sum a) = M1 _ _ (M1 _ _ (M1 _ _ (K1 _ a)))
+
+This can reduce as soon as GHC sees we have Sum whatever! So then the
+NewtypeF-calculated constraint can constrain the type argument to whatever's
+required to wrap the new contents. Magic!
+-}
+
+-- | Wrap a value with a newtype constructor.
+pack :: Newtype n o => o -> n
+pack = coerce
+
+-- | Unwrap a newtype constructor from a value.
+unpack :: Newtype n o => n -> o
+unpack = coerce
+
+-- | Reverse the type of a "packer".
+--
+-- >>> op All (All True)
+-- True
+-- >>> op (Identity . Sum) (Identity (Sum 3))
+-- 3
+op :: Coercible a b
+ => (a `to` b)
+ -> b
+ -> a
+op _ = coerce
+{-# INLINE op #-}
+
+-- | The workhorse of the package. Given a "packer" and a \"higher order function\" (/hof/),
+-- it handles the packing and unpacking, and just sends you back a regular old
+-- function, with the type varying based on the /hof/ you passed.
+--
+-- The reason for the signature of the /hof/ is due to 'ala' not caring about structure.
+-- To illustrate why this is important, consider this alternative implementation of 'under2':
+--
+-- > under2 :: (Newtype n o, Newtype n' o')
+-- > => (o -> n) -> (n -> n -> n') -> (o -> o -> o')
+-- > under2' pa f o0 o1 = ala pa (\p -> uncurry f . bimap p p) (o0, o1)
+--
+-- Being handed the "packer", the /hof/ may apply it in any structure of its choosing –
+-- in this case a tuple.
+--
+-- >>> ala Sum foldMap [1,2,3,4]
+-- 10
+ala :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> ((o -> n) -> b -> n') -> (b -> o')
+ala pa hof = ala' pa hof id
+
+-- | This is the original function seen in Conor McBride's work.
+-- The way it differs from the 'ala' function in this package,
+-- is that it provides an extra hook into the \"packer\" passed to the hof.
+-- However, this normally ends up being @id@, so 'ala' wraps this function and
+-- passes @id@ as the final parameter by default.
+-- If you want the convenience of being able to hook right into the hof,
+-- you may use this function.
+--
+-- >>> ala' Sum foldMap length ["hello", "world"]
+-- 10
+--
+-- >>> ala' First foldMap (readMaybe @Int) ["x", "42", "1"]
+-- Just 42
+ala' :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> ((a -> n) -> b -> n') -> (a -> o) -> (b -> o')
+--ala' _ hof f = unpack . hof (coerce . f)
+ala' _ = coerce
+
+-- | A very simple operation involving running the function \'under\' the newtype.
+--
+-- >>> under Product (stimes 3) 3
+-- 27
+under :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> (n -> n') -> (o -> o')
+under _ f = unpack #. f .# coerce
+
+-- | The opposite of 'under'. I.e., take a function which works on the
+-- underlying types, and switch it to a function that works on the newtypes.
+--
+-- >>> over All not (All False)
+-- All {getAll = True}
+over :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> (o -> o') -> (n -> n')
+over _ f = pack #. f .# coerce
+
+-- | Lower a binary function to operate on the underlying values.
+--
+-- >>> under2 Any (<>) True False
+-- True
+under2 :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> (n -> n -> n') -> (o -> o -> o')
+--under2 _ f o0 o1 = unpack $ f (coerce o0) (coerce o1)
+under2 _ = coerce
+
+-- | The opposite of 'under2'.
+over2 :: (Newtype n o, Newtype n' o', Similar n n')
+ => (o `to` n) -> (o -> o -> o') -> (n -> n -> n')
+--over2 _ f n0 n1 = pack $ f (coerce n0) (coerce n1)
+over2 _ = coerce
+
+-- | 'under' lifted into a functor.
+underF :: ( Newtype n o, Coercible (f o) (f n)
+ , Coercible (g n') (g o'), Newtype n' o', Similar n n')
+ => (o `to` n) -> (f n -> g n') -> (f o -> g o')
+underF _ f = coerce #. f .# coerce
+
+-- | 'over' lifted into a functor.
+overF :: ( Newtype n o, Coercible (f n) (f o), Coercible (g o') (g n')
+ , Newtype n' o', Similar n n')
+ => (o `to` n) -> (f o -> g o') -> (f n -> g n')
+overF _ f = coerce #. f .# coerce
diff --git a/test/Spec.hs b/test/Spec.hs
index 04ed3df..9d2ed06 100644
--- a/test/Spec.hs
+++ b/test/Spec.hs
@@ -1,3 +1,104 @@
+{-# language PartialTypeSignatures #-}
+-- We definitely don't want to infer the types of the test functions
+-- based on how they're *used*; if their implementations and (partial)
+-- signatures aren't sufficient, then we don't want them to have
+-- Typeable instances.
+{-# language NoMonomorphismRestriction #-}
+{-# OPTIONS_GHC -Wno-partial-type-signatures #-}
+
+module Main (main) where
+import Data.Monoid (Sum (..), All (..))
+import CoercibleUtils.Newtype
+import Type.Reflection
+
+-- We don't want defaults making it look like things are working
+-- if they're not!
+default ()
+
+pack_test0 :: _ -> All
+pack_test0 = pack
+
+pack_test1a :: _ -> Sum Int
+pack_test1a = pack
+
+pack_test1b :: Int -> Sum _
+pack_test1b = pack
+
+unpack_test0 :: All -> _
+unpack_test0 = unpack
+
+unpack_test1a :: Sum Int -> _
+unpack_test1a = unpack
+
+unpack_test1b :: Sum _ -> Int
+unpack_test1b = unpack
+
+-- Fix n
+ala_test0a
+ :: (_ -> All) -> (_ -> Bool -> _) -> Bool -> _
+ala_test0a = ala
+
+-- Fix n'
+ala_test0b
+ :: (_ -> _) -> (_ -> Bool -> All) -> (Bool -> _)
+ala_test0b = ala
+
+-- Fix o and o', partially fix n
+ala_test1a :: (Integer -> Sum _) -> (_ -> [Integer] -> _) -> [Integer] -> Word
+ala_test1a = ala
+ -- => (o `to` n) -> ((o -> n) -> b -> n') -> (b -> o')
+
+-- Fix o', partially fix n, and partially fix n'
+ala_test1b :: (_ -> Sum _) -> ((_ -> _ Integer) -> [Integer] -> _) -> [Integer] -> Word
+ala_test1b = ala
+
+-- Fix o and n'; infer o' and n
+ala_test1c :: (Integer -> _) -> ((_ -> _) -> [Integer] -> Sum Word) -> [Integer] -> _
+ala_test1c = ala
+
+-- Fix o' and n; infer o and n'
+ala_test1d :: (_ -> Sum Integer) -> (_ -> [Integer] -> _) -> [Integer] -> Word
+ala_test1d = ala
+
+under_test0a :: (_ -> All) -> _ -> _ -> _
+under_test0a = under
+
+under_test0b :: (_ -> _) -> (_ -> All) -> _ -> _
+under_test0b = under
+
+over_test0a :: (_ -> All) -> _ -> _ -> _
+over_test0a = over
+
+over_test0b :: (_ -> _) -> _ -> _ -> All
+over_test0b = over
+
main :: IO ()
-main = putStrLn ("Test suite not yet implemented" :: String)
+main = do
+ print $ (pack True :: All)
+ print $ unpack (All True)
+ print $ ala Sum foldMap [1..10 :: Int]
+ print $ under Sum (fmap (+1)) (3 :: Int)
+ print $ over Sum (+3) (Sum (3 :: Int))
+
+ -- Make sure the types are monomorphic. This is guaranteed by the
+ -- fact that the Typeable instances are resolved. Also make sure these
+ -- functions have the expected types!
+ print $ typeOf pack_test0
+ print $ typeOf pack_test1a
+ print $ typeOf pack_test1b
+ print $ typeOf unpack_test0
+ print $ typeOf unpack_test1a
+ print $ typeOf unpack_test1b
+
+ print $ typeOf ala_test0a
+ print $ typeOf ala_test0b
+ print $ typeOf ala_test1a
+ print $ typeOf ala_test1b
+ print $ typeOf ala_test1c
+ print $ typeOf ala_test1d
+
+ print $ typeOf under_test0a
+ print $ typeOf under_test0b
+ print $ typeOf over_test0a
+ print $ typeOf over_test0b