    {-# 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