content: {-# 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 (..))
  
  {-
    Note [Changing type parameters]
    ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
  
    To get good type inference for type-changing lenses, we want to be able
    map the field's type back to the type argument it corresponds to. This way,
    when the field is changed, we know what the result type of the structure is
    going to be.
  
    However, for a given type @t@, its representation @Rep t@ forgets which types
    in the structure came from type variables, and which didn't. An @Int@ that
    results from the instantiation of the type paremeter and an @Int@ that was
    monomorphically specified in the structure are indistinguishable.
  
    The solution is to replace the type arguments in the type with unique
    proxies, like: @T a b@ -> @T (P 1 a) (P 0 b)@. This way, if looking up
    a field's type yields something of shape @P _ _@, we know it came from a type
    parameter, and also know which.
  
    If the field's type is a proxy, then its type is allowed to change, otherwise
    not. This also allows us to satisfy the functional dependency @s field b -> t@.
    If after doing the conversion on @s@, @field@'s type is @(P _ a), then @t@ is
    @s[b/a]@, otherwise @t ~ s@ and @b ~ a@.
  -}
  
  -- `P` can be used in place of any type parameter, which means that it can have
  -- any kind, not just *, so a data type won't work.
  -- (this caused https://github.com/kcsongor/generic-lens/issues/23)
  -- Instead, we use a matchable type family to wrap any `k` - however, we can no longer directly
  -- pattern match on `P`, as it's not a type constructor. But we can still take it apart as a polymorphic
  -- application form. In order to distinguish between applications of P and other type constructors, we use a tag, `PTag`
  -- to fake a type constructor.
  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
  
  --------------------------------------------------------------------------------
  
  -- [TODO]: work this out
  --
  --type family ArgKind (t :: k) (pos :: Nat) :: * where
  --  ArgKind (t (a :: k)) 'Z = k
  --  ArgKind (t _) ('S pos) = ArgKind t pos
  --
  --type family ReplaceArg (t :: k) (pos :: Nat) (to :: ArgKind t pos) :: k where
  --  ReplaceArg (t a) 'Z to = t to
  --  ReplaceArg (t a) ('S pos) to = ReplaceArg t pos to a
  --  ReplaceArg t _ _ = t
  
  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)
  
  
  -- | Ensure that the types @a@ and @b@ are both applications of the same
  -- constructor. The arguments may be different.
  class UnifyHead (a :: k) (b :: k)
  instance {-# OVERLAPPING #-} (gb ~ g b, UnifyHead f g) => UnifyHead (f a) gb
  instance (a ~ b) => UnifyHead a b
  