@@ -12,12 +12,10 @@ module Data.Generics.Internal.Families.Changing
1212 ( Proxied
1313 , Infer
1414 , PTag (..)
15− , Peano (..)
16− , NatToPeano
1715 , P
1816 ) where
1917
20−import GHC.TypeLits (Nat, type (-), TypeError, ErrorMessage (..))
18+import GHC.TypeLits (Nat, type (-), type (+), TypeError, ErrorMessage (..))
2119
2220{-
2321 Note [Changing type parameters]
@@ -52,16 +50,16 @@ import GHC.TypeLits (Nat, type (-), TypeError, ErrorMessage (..))
5250-- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
5351-- to fake a type constructor.
5452data PTag = PTag
55−type family P :: Peano -> k -> PTag -> k
53+type family P :: Nat -> k -> PTag -> k
5654
57−type Proxied t = Proxied' t 'Z
55+type Proxied t = Proxied' t 0
5856
59−type family Proxied' (t :: k) (next :: Peano) :: k where
60− Proxied' (t (a :: j) :: k) next = (Proxied' t ('S next)) (P next a 'PTag)
57+type family Proxied' (t :: k) (next :: Nat) :: k where
58+ Proxied' (t (a :: j) :: k) next = (Proxied' t (next + 1)) (P next a 'PTag)
6159 Proxied' t _ = t
6260
6361data Sub where
64− Sub :: Peano -> k -> Sub
62+ Sub :: Nat -> k -> Sub
6563
6664type family Unify (a :: k) (b :: k) :: [Sub] where
6765 Unify (p n _ 'PTag) a' = '[ 'Sub n a']
@@ -85,26 +83,20 @@ type family Infer (s :: *) (a' :: *) (b :: *) :: * where
8583
8684--------------------------------------------------------------------------------
8785
88−data Peano = Z | S Peano
89−
90−type family NatToPeano (n :: Nat) :: Peano where
91− NatToPeano 0 = 'Z
92− NatToPeano n = 'S (NatToPeano (n - 1))
93−
9486-- [TODO]: work this out
9587--
96−--type family ArgKind (t :: k) (pos :: Peano) :: * where
88+--type family ArgKind (t :: k) (pos :: Nat) :: * where
9789-- ArgKind (t (a :: k)) 'Z = k
9890-- ArgKind (t _) ('S pos) = ArgKind t pos
9991--
100−--type family ReplaceArg (t :: k) (pos :: Peano) (to :: ArgKind t pos) :: k where
92+--type family ReplaceArg (t :: k) (pos :: Nat) (to :: ArgKind t pos) :: k where
10193-- ReplaceArg (t a) 'Z to = t to
10294-- ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
10395-- ReplaceArg t _ _ = t
10496
105−type family ReplaceArg (t :: k) (pos :: Peano) (to :: j) :: k where
106− ReplaceArg (t a) 'Z to = t to
107− ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
97+type family ReplaceArg (t :: k) (pos :: Nat) (to :: j) :: k where
98+ ReplaceArg (t a) 0 to = t to
99+ ReplaceArg (t a) pos to = ReplaceArg t (pos - 1) to a
108100 ReplaceArg t _ _ = t
109101
110102type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where