Modified error output and new tests for PolyKinds commit

testsuite/tests/arrows/should_fail/T5380.stderr

@@ -4,7 +4,7 @@ T5380.hs:7:27:
       `not_bool' is a rigid type variable bound by
                  the type signature for
                    testB :: not_bool -> (() -> ()) -> () -> not_unit
-                 at T5380.hs:7:1
+                 at T5380.hs:6:10
     In the expression: b
     In the expression: proc () -> if b then f -< () else f -< ()
     In an equation for `testB':
@@ -15,7 +15,7 @@ T5380.hs:7:34:
       `not_unit' is a rigid type variable bound by
                  the type signature for
                    testB :: not_bool -> (() -> ()) -> () -> not_unit
-                 at T5380.hs:7:1
+                 at T5380.hs:6:42
     Expected type: () -> not_unit
       Actual type: () -> ()
     In the expression: f

testsuite/tests/gadt/rw.stderr

@@ -3,7 +3,7 @@ rw.hs:14:47:
     Couldn't match expected type `a' with actual type `Int'
       `a' is a rigid type variable bound by
           the type signature for writeInt :: T a -> IORef a -> IO ()
-          at rw.hs:13:1
+          at rw.hs:12:14
     In the second argument of `writeIORef', namely `(1 :: Int)'
     In the expression: writeIORef ref (1 :: Int)
     In a case alternative: ~(Li x) -> writeIORef ref (1 :: Int)
@@ -12,7 +12,7 @@ rw.hs:19:51:
     Couldn't match type `a' with `Bool'
       `a' is a rigid type variable bound by
           the type signature for readBool :: T a -> IORef a -> IO ()
-          at rw.hs:17:1
+          at rw.hs:16:14
     Expected type: a -> Bool
       Actual type: Bool -> Bool
     In the second argument of `(.)', namely `not'

testsuite/tests/ghci/scripts/Defer02.stderr

@@ -37,7 +37,7 @@
     Couldn't match expected type `a' with actual type `Char'
       `a' is a rigid type variable bound by
           the type signature for h :: a -> (Char, Char)
-          at ../../typecheck/should_run/Defer01.hs:34:1
+          at ../../typecheck/should_run/Defer01.hs:33:6
     In the expression: x
     In the expression: (x, 'c')
     In an equation for `h': h x = (x, 'c')

testsuite/tests/ghci/scripts/Defer02.stdout

@@ -36,7 +36,7 @@ Hello World*** Exception: ../../typecheck/should_run/Defer01.hs:11:40:
     Couldn't match expected type `a' with actual type `Char'
       `a' is a rigid type variable bound by
           the type signature for h :: a -> (Char, Char)
-          at ../../typecheck/should_run/Defer01.hs:34:1
+          at ../../typecheck/should_run/Defer01.hs:33:6
     In the expression: x
     In the expression: (x, 'c')
     In an equation for `h': h x = (x, 'c')

testsuite/tests/indexed-types/should_compile/Simple14.stderr

@@ -7,7 +7,7 @@ Simple14.hs:17:12:
                       Maybe m ~ Maybe n => EQ_ z0 z0
       `n' is a rigid type variable bound by
           the type signature for foo :: EQ_ (Maybe m) (Maybe n)
-          at Simple14.hs:17:1
+          at Simple14.hs:16:17
     Expected type: EQ_ z0 z0
       Actual type: EQ_ m n
     In the second argument of `eqE', namely `(eqI :: EQ_ m n)'

testsuite/tests/indexed-types/should_compile/T3208b.stderr

@@ -4,7 +4,7 @@ T3208b.hs:15:10:
     from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for
                  fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-      at T3208b.hs:15:1-22
+      at T3208b.hs:14:9-56
     NB: `STerm' is a type function, and may not be injective
     The type variable `a0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
@@ -18,7 +18,7 @@ T3208b.hs:15:15:
     from the context (OTerm a ~ STerm a, OBJECT a, SUBST a)
       bound by the type signature for
                  fce' :: (OTerm a ~ STerm a, OBJECT a, SUBST a) => a -> c
-      at T3208b.hs:15:1-22
+      at T3208b.hs:14:9-56
     The type variable `a0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     In the first argument of `fce', namely `(apply f)'

testsuite/tests/indexed-types/should_compile/all.T

@@ -21,7 +21,7 @@ test('Simple16', normal, compile, [''])
 test('Simple17', normal, compile, [''])
 test('Simple18', normal, compile, [''])
 test('Simple19', normal, compile, [''])
-test('Simple20', expect_broken(4296), compile, ['-fcontext-stack=50'])
+test('Simple20', expect_broken(4296), compile, ['-fcontext-stack=10'])
 test('Simple21', normal, compile, [''])
 test('Simple22', normal, compile, [''])
 test('Simple23', normal, compile, [''])

testsuite/tests/indexed-types/should_fail/GADTwrong1.stderr

@@ -7,7 +7,7 @@ GADTwrong1.hs:12:19:
                in a case alternative
       at GADTwrong1.hs:12:12-14
       `b' is a rigid type variable bound by
-          the type signature for coerce :: a -> b at GADTwrong1.hs:11:1
+          the type signature for coerce :: a -> b at GADTwrong1.hs:10:20
       `a1' is a rigid type variable bound by
            a pattern with constructor
              T :: forall a. a -> T (Const a),

testsuite/tests/indexed-types/should_fail/NoMatchErr.stderr

@@ -3,7 +3,7 @@ NoMatchErr.hs:20:5:
     Could not deduce (Memo d ~ Memo d0)
     from the context (Fun d)
       bound by the type signature for f :: Fun d => Memo d a -> Memo d a
-      at NoMatchErr.hs:20:1-15
+      at NoMatchErr.hs:19:7-37
     NB: `Memo' is a type function, and may not be injective
     The type variable `d0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)

testsuite/tests/indexed-types/should_fail/SimpleFail15.stderr

-
-SimpleFail15.hs:5:1:
-    Illegal polymorphic or qualified type: a ~ b => t
-    Perhaps you intended to use -XRankNTypes or -XRank2Types
-    In the type signature for `foo':
-      foo :: (a, b) -> (a ~ b => t) -> (a, b)
+
+SimpleFail15.hs:5:8:
+    Illegal polymorphic or qualified type: a ~ b => t
+    Perhaps you intended to use -XRankNTypes or -XRank2Types
+    In the type signature for `foo':
+      foo :: (a, b) -> (a ~ b => t) -> (a, b)

testsuite/tests/indexed-types/should_fail/SimpleFail5a.stderr

@@ -3,7 +3,7 @@ SimpleFail5a.hs:31:11:
     Couldn't match type `a' with `Int'
       `a' is a rigid type variable bound by
           the type signature for bar3wrong :: S3 a -> a
-          at SimpleFail5a.hs:31:1
+          at SimpleFail5a.hs:30:17
     Expected type: S3 a
       Actual type: S3 Int
     In the pattern: D3Int

testsuite/tests/indexed-types/should_fail/SimpleFail6.stderr

 
-SimpleFail6.hs:7:11: Illegal repeated type variable `a'
+SimpleFail6.hs:7:11:
+    Conflicting definitions for `a'
+    Bound at: SimpleFail6.hs:7:11
+              SimpleFail6.hs:7:13

testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.hs

-{-# OPTIONS_GHC -fcontext-stack=10 #-}
+{-# OPTIONS_GHC -fcontext-stack=3 #-}
 {-# LANGUAGE TypeFamilies, FlexibleContexts, EmptyDataDecls #-}
 
 module SkolemOccursLoop where

testsuite/tests/indexed-types/should_fail/SkolemOccursLoop.stderr

-
-SkolemOccursLoop.hs:18:0:
-    Couldn't match expected type `F a'
-           against inferred type `[T (F (T (F a)))]'
-    When generalising the type(s) for `test1'
-
-SkolemOccursLoop.hs:31:0:
-    Couldn't match expected type `S (G (a, a))'
-           against inferred type `G [S (G (a, a))]'
-    When generalising the type(s) for `test2'
+Skolem occurs loop 

testsuite/tests/indexed-types/should_fail/T1900.stderr

@@ -11,7 +11,7 @@ T1900.hs:14:22:
     Could not deduce (Depend s0 ~ Depend s)
     from the context (Bug s)
       bound by the type signature for check :: Bug s => Depend s -> Bool
-      at T1900.hs:14:1-22
+      at T1900.hs:13:10-36
     NB: `Depend' is a type function, and may not be injective
     The type variable `s0' is ambiguous
     Possible fix: add a type signature that fixes these type variable(s)

testsuite/tests/indexed-types/should_fail/T3330a.stderr

-
-T3330a.hs:19:34:
-    Couldn't match type `s' with `(->) (s0 ix1 -> ix1)'
-      `s' is a rigid type variable bound by
-          the type signature for children :: s ix -> PF s r ix -> [AnyF s]
-          at T3330a.hs:19:1
-    Expected type: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r ix1)
-      Actual type: s ix
-    In the first argument of `hmapM', namely `p'
-    In the first argument of `execWriter', namely `(hmapM p collect x)'
-    In the expression: execWriter (hmapM p collect x)
-
-T3330a.hs:19:36:
-    Couldn't match type `ix' with `r ix0 -> Writer [AnyF s0] (r ix0)'
-      `ix' is a rigid type variable bound by
-           the type signature for children :: s ix -> PF s r ix -> [AnyF s]
-           at T3330a.hs:19:1
-    Expected type: s0 ix0 -> ix
-      Actual type: s0 ix0 -> r ix0 -> Writer [AnyF s0] (r ix0)
-    In the second argument of `hmapM', namely `collect'
-    In the first argument of `execWriter', namely `(hmapM p collect x)'
-    In the expression: execWriter (hmapM p collect x)
+
+T3330a.hs:19:34:
+    Couldn't match type `s' with `(->) (s0 ix1 -> ix1)'
+      `s' is a rigid type variable bound by
+          the type signature for children :: s ix -> PF s r ix -> [AnyF s]
+          at T3330a.hs:18:13
+    Expected type: (s0 ix0 -> ix1) -> r ix1 -> Writer [AnyF s] (r ix1)
+      Actual type: s ix
+    In the first argument of `hmapM', namely `p'
+    In the first argument of `execWriter', namely `(hmapM p collect x)'
+    In the expression: execWriter (hmapM p collect x)
+
+T3330a.hs:19:36:
+    Couldn't match type `ix' with `r ix0 -> Writer [AnyF s0] (r ix0)'
+      `ix' is a rigid type variable bound by
+           the type signature for children :: s ix -> PF s r ix -> [AnyF s]
+           at T3330a.hs:18:15
+    Expected type: s0 ix0 -> ix
+      Actual type: s0 ix0 -> r ix0 -> Writer [AnyF s0] (r ix0)
+    In the second argument of `hmapM', namely `collect'
+    In the first argument of `execWriter', namely `(hmapM p collect x)'
+    In the expression: execWriter (hmapM p collect x)

testsuite/tests/indexed-types/should_fail/T3440.stderr

@@ -8,7 +8,7 @@ T3440.hs:11:22:
       at T3440.hs:11:9-16
       `a' is a rigid type variable bound by
           the type signature for unwrap :: GADT (Fam a) -> (a, Fam a)
-          at T3440.hs:11:1
+          at T3440.hs:10:21
       `a1' is a rigid type variable bound by
            a pattern with constructor
              GADT :: forall a. a -> Fam a -> GADT (Fam a),

testsuite/tests/indexed-types/should_fail/T4093a.stderr

@@ -3,10 +3,10 @@ T4093a.hs:8:8:
     Could not deduce (e ~ ())
     from the context (Foo e ~ Maybe e)
       bound by the type signature for hang :: Foo e ~ Maybe e => Foo e
-      at T4093a.hs:8:1-14
+      at T4093a.hs:7:9-34
       `e' is a rigid type variable bound by
           the type signature for hang :: Foo e ~ Maybe e => Foo e
-          at T4093a.hs:8:1
+          at T4093a.hs:7:14
     Expected type: Foo e
       Actual type: Maybe ()
     In the return type of a call of `Just'

testsuite/tests/indexed-types/should_fail/T4093b.stderr

@@ -7,13 +7,13 @@ T4093b.hs:31:13:
                  blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,
                                      EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                                     Block n e x -> A e x n
-      at T4093b.hs:(25,1)-(34,19)
+      at T4093b.hs:(20,3)-(22,26)
       `e' is a rigid type variable bound by
           the type signature for
             blockToNodeList :: (EitherCO e (A C O n) (A O O n) ~ A e O n,
                                 EitherCO x (A C C n) (A C O n) ~ A C x n) =>
                                Block n e x -> A e x n
-          at T4093b.hs:25:1
+          at T4093b.hs:20:12
     Expected type: EitherCO e (A C O n) (A O O n)
       Actual type: (MaybeC C (n C O), MaybeC O (n O C))
     In the expression: (JustC n, NothingC)

testsuite/tests/indexed-types/should_fail/T4179.stderr

@@ -6,7 +6,7 @@ T4179.hs:26:16:
       bound by the type signature for
                  fCon :: (Functor x, DoC (FCon x)) =>
                          Con x -> A2 (FCon x) -> A3 (FCon x)
-      at T4179.hs:26:1-17
+      at T4179.hs:25:9-72
     NB: `A3' is a type function, and may not be injective
     Expected type: x (A2 (x (Con x)) -> A3 (x (Con x)))
                    -> A2 (x (Con x)) -> A3 (x (Con x))

testsuite/tests/indexed-types/should_fail/T4272.stderr

@@ -27,10 +27,10 @@ T4272.hs:11:19:
     from the context (TermLike a)
       bound by the type signature for
                  laws :: TermLike a => TermFamily a a -> b
-      at T4272.hs:11:1-54
+      at T4272.hs:10:9-53
       `a' is a rigid type variable bound by
           the type signature for laws :: TermLike a => TermFamily a a -> b
-          at T4272.hs:11:1
+          at T4272.hs:10:16
     In the return type of a call of `terms'
     In the second argument of `prune', namely
       `(terms (undefined :: TermFamily a a))'

testsuite/tests/module/mod45.stderr

-
-mod45.hs:5:3:
-    Illegal type signature in instance declaration:
-      (==) :: T -> T -> Bool
-    (Use -XInstanceSigs to allow this)
-    In the instance declaration for `Eq T'
+
+mod45.hs:5:11:
+    Illegal type signature in instance declaration:
+      (==) :: T -> T -> Bool
+    (Use -XInstanceSigs to allow this)
+    In the instance declaration for `Eq T'

testsuite/tests/parser/should_fail/readFail036.stderr

 
-readFail036.hs:4:1:
-    Illegal kind signature for `a'
+readFail036.hs:4:16:
+    Illegal kind signature: `*'
       Perhaps you intended to use -XKindSignatures
+    In the data type declaration for `Foo'

testsuite/tests/perf/compiler/all.T

@@ -24,7 +24,7 @@ test('T1969',
                              #                 5717704 (x86/Windows 17/05/10)
                              #                 6149572 (x86/Linux, 31/12/09)
       if_wordsize(64,
-          compiler_stats_range_field('max_bytes_used', 11178376, 10)),
+          compiler_stats_range_field('max_bytes_used', 12000000, 10)),
                                    # expected value: 11178376 (amd64/Linux)
       if_wordsize(32,
           compiler_stats_num_field('bytes allocated', 210000000,

testsuite/tests/polykinds/Freeman.hs

+-- From the blog post Fun With XPolyKinds : Polykinded Folds
+--   http://www.typesandotherdistractions.com/2012/02/fun-with-xpolykinds-polykinded-folds.html
+
+{-
+In the following, I will write a polykinded version of the combinators
+fold and unfold, along with three examples: folds for regular
+datatypes (specialized to kind *), folds for nested datatypes
+(specialized to kind * -> *), and folds for mutually recursive data
+types (specialized to the product kind (*,*)). The approach should
+generalise easily enough to things such as types indexed by another
+kind (e.g. by specializing to kind Nat -> *, using the XDataKinds
+extension), or higher order nested datatypes (e.g. by specializing to
+kind (* -> *) -> (* -> *)).
+
+The following will compile in the new GHC 7.4.1 release. We require
+the following GHC extensions:
+-}
+
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE PolyKinds #-}
+{-# LANGUAGE KindSignatures #-}
+{-# LANGUAGE DataKinds #-}
+{-# LANGUAGE RankNTypes #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE MultiParamTypeClasses #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE StandaloneDeriving #-}
+module Main where
+
+{- The basic fold and unfold combinators can be written as follows:
+
+fold phi = phi . fmap (fold phi) . out
+unfold psi = in . fmap (unfold psi) . psi
+
+The idea now is to generalize these combinators by working over
+different categories. We can capture the basic operations in a
+category with a typeclass: -}
+
+class Category hom where
+  ident :: hom a a
+  compose :: hom a b -> hom b c -> hom a c
+
+{- A category has two operations: an identity morphism for every
+object, and for every two compatible morphisms, the composition of
+those morphisms.
+
+In earlier versions of GHC, the type hom would have been specialized
+to kind * -> * -> *, but with the new PolyKinds extension, hom is
+polykinded, and the Category typeclass can be instantiated to k -> k
+-> * for any kind k. This means that in addition to all of the
+Category instances that we could have written before, we can now write
+instances of Category for type constructors, type constructor
+constructors, etc.
+
+Here is the instance for the category Hask of Haskell types. Objects
+are Haskell types and morphisms are functions between types. The
+identity is the regular polymorphic identity function id, and
+composition is given by the (flipped) composition operator (.) -}
+
+instance Category (->) where
+  ident = id
+  compose = flip (.)
+
+{- Another example is the category of type constructors and natural
+transformations. A natural transformation is defined as follows: -}
+
+newtype Nat f g = Nat { nu :: (forall a. f a -> g a) } 
+
+{- Here is the Category instance for natural transformations. This
+time the type hom is inferred to have kind (* -> *) -> (* -> *) ->
+*. Identity and composition are both defined pointwise. -}
+
+instance Category (Nat :: (* -> *) -> (* -> *) -> *) where
+  ident = Nat id
+  compose f g = Nat (nu g . nu f)
+
+{- Let's define a type class which will capture the idea of a fixed point
+in a category. This generalizes the idea of recursive types in Hask: -}
+
+class Rec hom f t where
+  _in :: hom (f t) t
+  out :: hom t (f t)
+
+{- The class Rec defines two morphisms: _in, which is the constructor of
+the fixed point type t, and out, its destructor.
+
+The final piece is the definition of a higher order functor, which
+generalizes the typeclass Functor: -}
+
+class HFunctor hom f where
+  hmap :: hom a b -> hom (f a) (f b)
+
+{- Note the similarity with the type signature of the function fmap ::
+(Functor f) => (a -> b) -> f a -> f b. Indeed, specializing hom to
+(->) in the definition of HFunctor gives back the type signature of
+fmap. 
+
+Finally, we can define folds and unfolds in a category. The
+definitions are as before, but with explicit composition, constructors
+and destructors replaced with the equivalent type class methods, and
+hmap in place of fmap: -}
+
+fold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom (f t) t -> hom rec t
+fold phi = compose out (compose (hmap (fold phi)) phi)
+
+unfold :: (Category hom, HFunctor hom f, Rec hom f rec) => hom t (f t) -> hom t rec
+unfold phi = compose phi (compose (hmap (unfold phi)) _in)
+
+-- Now for some examples.
+
+-- The first example is a regular recursive datatype of binary leaf
+-- trees. The functor FTree is the base functor of this recursive type:
+
+data FTree a b = FLeaf a | FBranch b b
+data Tree a = Leaf a | Branch (Tree a) (Tree a)
+
+-- An instance of Rec shows the relationship between the defining functor
+-- and the recursive type itself:
+
+instance Rec (->) (FTree a) (Tree a) where
+  _in (FLeaf a) = Leaf a
+  _in (FBranch a b) = Branch a b
+  out (Leaf a) = FLeaf a
+  out (Branch a b) = FBranch a b
+
+-- FTree is indeed a functor, so it is also a HFunctor:
+
+instance HFunctor (->) (FTree a) where
+  hmap f (FLeaf a) = FLeaf a
+  hmap f (FBranch a b) = FBranch (f a) (f b)
+
+-- These instances are enough to define folds and unfolds for this
+-- type. The following fold calculates the depth of a tree:
+
+depth :: Tree a -> Int
+depth = (fold :: (FTree a Int -> Int) -> Tree a -> Int) phi where
+  phi :: FTree a Int -> Int
+  phi (FLeaf a) = 1
+  phi (FBranch a b) = 1 + max a b
+
+-- The second example is a fold for the nested (or non-regular)
+-- datatype of complete binary leaf trees. The higher order functor
+-- FCTree defines the type constructor CTree as its fixed point:
+
+data FCTree f a = FCLeaf a | FCBranch (f (a, a))
+  -- FCTree :: (* -> *) -> * -> *
+
+data CTree a = CLeaf a | CBranch (CTree (a, a))
+
+-- Again, we define type class instances for HFunctor and Rec:
+
+instance HFunctor Nat FCTree where
+  hmap (f :: Nat (f :: * -> *) (g :: * -> *)) = Nat ff where
+    ff :: forall a. FCTree f a -> FCTree g a
+    ff (FCLeaf a) = FCLeaf a
+    ff (FCBranch a) = FCBranch (nu f a)
+
+instance Rec Nat FCTree CTree where
+  _in = Nat inComplete where
+    inComplete (FCLeaf a) = CLeaf a
+    inComplete (FCBranch a) = CBranch a
+  out = Nat outComplete where
+    outComplete(CLeaf a) = FCLeaf a
+    outComplete(CBranch a) = FCBranch a
+
+-- Morphisms between type constructors are natural transformations, so we
+-- need a type constructor to act as the target of the fold. For our
+-- purposes, a constant functor will do:
+
+data K a b = K a  -- K :: forall k. * -> k -> *
+
+
+-- And finally, the following fold calculates the depth of a complete binary leaf tree:
+
+cdepth :: CTree a -> Int
+cdepth c = let (K d) = nu (fold (Nat phi)) c in d where
+  phi :: FCTree (K Int) a -> K Int a
+  phi (FCLeaf a) = K 1
+  phi (FCBranch (K n)) = K (n + 1)
+
+{- The final example is a fold for the pair of mutually recursive
+datatype of lists of even and odd lengths. The fold will take a list
+of even length and produce a list of pairs.
+
+We cannot express type constructors in Haskell whose return kind is
+anything other than *, so we cheat a little and emulate the product
+kind using an arrow kind Choice -> *, where Choice is a two point
+kind, lifted using the XDataKinds extension: -}
+
+data Choice = Fst | Snd
+
+-- A morphism of pairs of types is just a pair of morphisms. For
+-- technical reasons, we represent this using a Church-style encoding,
+-- along with helper methods, as follows:
+
+newtype PHom h1 h2 p1 p2 = PHom { runPHom :: forall r. (h1 (p1 Fst) (p2 Fst) -> h2 (p1 Snd) (p2 Snd) -> r) -> r }
+
+mkPHom f g = PHom (\h -> h f g)
+fstPHom p = runPHom p (\f -> \g -> f)
+sndPHom p = runPHom p (\f -> \g -> g)
+
+-- Now, PHom allows us to take two categories and form the product category:
+
+instance (Category h1, Category h2) => Category (PHom h1 h2) where
+  ident = mkPHom ident ident
+  compose p1 p2 = mkPHom (compose (fstPHom p1) (fstPHom p2)) (compose (sndPHom p1) (sndPHom p2))
+
+-- We can define the types of lists of even and odd length as
+-- follows. Note that the kind annotation indicates the appearance of the
+-- kind Choice -> *:
+
+data FAlt :: * -> (Choice -> *) -> Choice -> * where
+  FZero :: FAlt a p Fst
+  FSucc1 :: a -> (p Snd) -> FAlt a p Fst
+  FSucc2 :: a -> (p Fst) -> FAlt a p Snd
+
+data Alt :: * -> Choice -> * where
+  Zero :: Alt a Fst
+  Succ1 :: a -> Alt a Snd -> Alt a Fst
+  Succ2 :: a -> Alt a Fst -> Alt a Snd
+
+deriving instance Show a => Show (Alt a b)
+
+-- Again, we need to define instances of Rec and HFunctor:
+
+instance Rec (PHom (->) (->)) (FAlt a) (Alt a) where
+  _in = mkPHom f g where
+    f FZero = Zero
+    f (FSucc1 a b) = Succ1 a b
+    g (FSucc2 a b) = Succ2 a b
+  out = mkPHom f g where
+    f Zero = FZero
+    f (Succ1 a b) = FSucc1 a b
+    g (Succ2 a b) = FSucc2 a b
+
+instance HFunctor (PHom (->) (->)) (FAlt a) where
+  hmap p = mkPHom hf hg where
+    hf FZero = FZero
+    hf (FSucc1 a x) = FSucc1 a (sndPHom p x)
+    hg (FSucc2 a x) = FSucc2 a (fstPHom p x)
+
+-- As before, we create a target type for our fold, and this time a type synonym as well:
+
+data K2 :: * -> * -> Choice -> * where
+  K21 :: a -> K2 a b Fst
+  K22 :: b -> K2 a b Snd
+
+type PairUpResult a = K2 [(a, a)] (a, [(a, a)])
+
+-- At last, here is the fold pairUp, taking even length lists to lists of pairs:
+
+pairUp :: Alt a Fst -> [(a, a)]
+pairUp xs = let (K21 xss) = (fstPHom (fold (mkPHom phi psi))) xs in xss 
+ where
+   phi FZero = K21 []
+   phi (FSucc1 x1 (K22 (x2, xss))) = K21 ((x1, x2):xss) 
+   psi (FSucc2 x (K21 xss)) = K22 (x, xss) 
+
+main = print (Succ1 (0::Int) $ Succ2 1 $ Succ1 2 $ Succ2 3 $ Succ1 4 $ Succ2 5 Zero)

testsuite/tests/polykinds/Freeman.stdout

+Succ1 0 (Succ2 1 (Succ1 2 (Succ2 3 (Succ1 4 (Succ2 5 Zero)))))