{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
module Data.Generics.Internal.Families.Changing
( Indexed
, Infer
, PTag (..)
, P
, LookupParam
, ArgAt
, ArgCount
, UnifyHead
) where
import GHC.TypeLits (Nat, type (-), type (+), TypeError, ErrorMessage (..))
data PTag = PTag
type family P :: Nat -> k -> PTag -> k
type Indexed t = Indexed' t 0
type family Indexed' (t :: k) (next :: Nat) :: k where
Indexed' (t (a :: j) :: k) next = (Indexed' t (next + 1)) (P next a 'PTag)
Indexed' t _ = t
data Sub where
Sub :: Nat -> k -> Sub
type family Unify (a :: k) (b :: k) :: [Sub] where
Unify (p n _ 'PTag) a' = '[ 'Sub n a']
Unify (a x) (b y) = Unify x y ++ Unify a b
Unify a a = '[]
Unify a b = TypeError
( 'Text "Couldn't match type "
':<>: 'ShowType a
':<>: 'Text " with "
':<>: 'ShowType b
)
type family (xs :: [k]) ++ (ys :: [k]) :: [k] where
'[] ++ ys = ys
(x ': xs) ++ ys = x ': (xs ++ ys)
type family Infer (s :: *) (a' :: *) (b :: *) :: * where
Infer (s a) a' b
= ReplaceArgs (s a) (Unify a' b)
Infer s _ _ = s
type family ReplaceArg (t :: k) (pos :: Nat) (to :: j) :: k where
ReplaceArg (t a) 0 to = t to
ReplaceArg (t a) pos to = ReplaceArg t (pos - 1) to a
ReplaceArg t _ _ = t
type family ReplaceArgs (t :: k) (subs :: [Sub]) :: k where
ReplaceArgs t '[] = t
ReplaceArgs t ('Sub n arg ': ss) = ReplaceArgs (ReplaceArg t n arg) ss
type family LookupParam (a :: k) (p :: Nat) :: Maybe Nat where
LookupParam (param (n :: Nat)) m = 'Nothing
LookupParam (a (_ (m :: Nat))) n = IfEq m n ('Just 0) (MaybeAdd (LookupParam a n) 1)
LookupParam (a _) n = MaybeAdd (LookupParam a n) 1
LookupParam a _ = 'Nothing
type family MaybeAdd (a :: Maybe Nat) (b :: Nat) :: Maybe Nat where
MaybeAdd 'Nothing _ = 'Nothing
MaybeAdd ('Just a) b = 'Just (a + b)
type family IfEq (a :: k) (b :: k) (t :: l) (f :: l) :: l where
IfEq a a t _ = t
IfEq _ _ _ f = f
type family ArgCount (t :: k) :: Nat where
ArgCount (f a) = 1 + ArgCount f
ArgCount a = 0
type family ArgAt (t :: k) (n :: Nat) :: j where
ArgAt (t a) 0 = a
ArgAt (t a) n = ArgAt t (n - 1)
class UnifyHead (a :: k) (b :: k)
instance {-# OVERLAPPING #-} (gb ~ g b, UnifyHead f g) => UnifyHead (f a) gb
instance (a ~ b) => UnifyHead a b