{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}

-- | Machinery for the 'Generic'-based 'HasDependencies' instance
module Graphula.Dependencies.Generic
  ( GHasDependencies (..)
  ) where

import Data.Kind (Type)
import GHC.TypeLits (ErrorMessage (..), TypeError)
import Generics.Eot (Proxy (..), Void)

data Match t
  = NoMatch t
  | Match t

type family DependenciesTypeInstance nodeTy depsTy where
  DependenciesTypeInstance nodeTy depsTy =
    'Text "‘type Dependencies "
      ':<>: 'ShowType nodeTy
      ':<>: 'Text " = "
      ':<>: 'ShowType depsTy
      ':<>: 'Text "’"

-- Walk through the fields of our node and match them up with fields from the dependencies.
type family FindMatches nodeTy depsTy as ds :: [Match Type] where
  -- Excess dependencies
  FindMatches nodeTy depsTy () (d, _ds) =
    TypeError
      ( 'Text "Excess dependency ‘"
          ':<>: 'ShowType d
          ':<>: 'Text "’ in "
          ':$$: DependenciesTypeInstance nodeTy depsTy
          ':$$: 'Text
                  "Ordering of dependencies must match their occurrence in the target type ‘"
          ':<>: 'ShowType nodeTy
          ':<>: 'Text "’"
      )
  -- No more fields or dependencies left
  FindMatches _nodeTy _depsTy () () = '[]
  -- Fields left, but no more dependencies
  FindMatches nodeTy depsTy (a, as) () =
    'NoMatch a ': FindMatches nodeTy depsTy as ()
  -- Field matches dependency, keep going
  FindMatches nodeTy depsTy (a, as) (a, ds) =
    'Match a ': FindMatches nodeTy depsTy as ds
  -- Field does not match dependency, keep going
  FindMatches nodeTy depsTy (a, as) (d, ds) =
    'NoMatch a ': FindMatches nodeTy depsTy as (d, ds)

class GHasDependencies nodeTyProxy depsTyProxy node deps where
  genericDependsOn :: nodeTyProxy -> depsTyProxy -> node -> deps -> node

class GHasDependenciesRecursive fieldsProxy node deps where
  genericDependsOnRecursive :: fieldsProxy -> node -> deps -> node

-- This instance head only matches EoT representations of
-- datatypes with no constructors and no dependencies
instance {-# OVERLAPPING #-} GHasDependencies (Proxy nodeTy) (Proxy depsTy) Void (Either () Void) where
  genericDependsOn :: Proxy nodeTy -> Proxy depsTy -> Void -> Either () Void -> Void
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Void
node Either () Void
_ = Void
node

-- This instance warns the user if they give dependencies
-- to a datatype with no constructors
instance
  {-# OVERLAPPABLE #-}
  TypeError
    ( 'Text "A datatype with no constructors can't use the dependencies in"
        ':$$: DependenciesTypeInstance nodeTy depsTy
    )
  => GHasDependencies (Proxy nodeTy) (Proxy depsTy) Void (Either deps rest)
  where
  genericDependsOn :: Proxy nodeTy -> Proxy depsTy -> Void -> Either deps rest -> Void
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Void
_ Either deps rest
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

-- This instance head only matches EoT representations of
-- datatypes with a single constructor
instance
  ( FindMatches nodeTy depsTy node deps ~ fields
  , GHasDependenciesRecursive (Proxy fields) node deps
  )
  => GHasDependencies
      (Proxy nodeTy)
      (Proxy depsTy)
      (Either node Void)
      (Either deps Void)
  where
  genericDependsOn :: Proxy nodeTy
-> Proxy depsTy
-> Either node Void
-> Either deps Void
-> Either node Void
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ (Left node
node) (Left deps
deps) =
    forall a b. a -> Either a b
Left (forall fieldsProxy node deps.
GHasDependenciesRecursive fieldsProxy node deps =>
fieldsProxy -> node -> deps -> node
genericDependsOnRecursive (forall {k} (t :: k). Proxy t
Proxy :: Proxy fields) node
node deps
deps)
  genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Either node Void
_ Either deps Void
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible" -- EoT never generates an actual `Right (x :: Void)` here

-- This instance matches a sum type as both node and dependencies.
-- We use this to report an error to the user.
instance
  TypeError
    ( 'Text "Cannot automatically find dependencies for sum type in"
        ':$$: DependenciesTypeInstance nodeTy depsTy
    )
  => GHasDependencies
      (Proxy nodeTy)
      (Proxy depsTy)
      (Either left (Either right rest))
      (Either deps Void)
  where
  genericDependsOn :: Proxy nodeTy
-> Proxy depsTy
-> Either left (Either right rest)
-> Either deps Void
-> Either left (Either right rest)
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Either left (Either right rest)
_ Either deps Void
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

-- This instance matches a sum type as the node.
-- This is also an error.
instance
  TypeError
    ( 'Text "Cannot automatically use a sum type as dependencies in"
        ':$$: DependenciesTypeInstance nodeTy depsTy
    )
  => GHasDependencies
      (Proxy nodeTy)
      (Proxy depsTy)
      (Either node Void)
      (Either left (Either right rest))
  where
  genericDependsOn :: Proxy nodeTy
-> Proxy depsTy
-> Either node Void
-> Either left (Either right rest)
-> Either node Void
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Either node Void
_ Either left (Either right rest)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

-- This instance matches a sum type as the dependencies.
-- This is also an error.
instance
  TypeError
    ( 'Text
        "Cannot automatically find dependencies for sum type or use a sum type as a dependency in"
        ':$$: DependenciesTypeInstance nodeTy depsTy
    )
  => GHasDependencies
      (Proxy nodeTy)
      (Proxy depsTy)
      (Either left1 (Either right1 rest1))
      (Either left2 (Either right2 rest2))
  where
  genericDependsOn :: Proxy nodeTy
-> Proxy depsTy
-> Either left1 (Either right1 rest1)
-> Either left2 (Either right2 rest2)
-> Either left1 (Either right1 rest1)
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ Either left1 (Either right1 rest1)
_ Either left2 (Either right2 rest2)
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

-- Don't let the user specify `Void` as a dependency
instance
  TypeError
    ( 'Text "Use ‘()’ instead of ‘Void’ for datatypes with no dependencies in"
        ':$$: DependenciesTypeInstance nodeTy depsTy
    )
  => GHasDependencies (Proxy nodeTy) (Proxy depsTy) node Void
  where
  genericDependsOn :: Proxy nodeTy -> Proxy depsTy -> node -> Void -> node
genericDependsOn Proxy nodeTy
_ Proxy depsTy
_ node
_ Void
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"Impossible"

instance
  ( a ~ dep
  , GHasDependenciesRecursive (Proxy fields) as deps
  )
  => GHasDependenciesRecursive (Proxy ('Match a ': fields)) (a, as) (dep, deps)
  where
  genericDependsOnRecursive :: Proxy ('Match a : fields) -> (a, as) -> (dep, deps) -> (a, as)
genericDependsOnRecursive Proxy ('Match a : fields)
_ (a
_, as
as) (dep
dep, deps
deps) =
    (dep
dep, forall fieldsProxy node deps.
GHasDependenciesRecursive fieldsProxy node deps =>
fieldsProxy -> node -> deps -> node
genericDependsOnRecursive (forall {k} (t :: k). Proxy t
Proxy :: Proxy fields) as
as deps
deps)

instance
  GHasDependenciesRecursive (Proxy fields) as deps
  => GHasDependenciesRecursive (Proxy ('NoMatch a ': fields)) (a, as) deps
  where
  genericDependsOnRecursive :: Proxy ('NoMatch a : fields) -> (a, as) -> deps -> (a, as)
genericDependsOnRecursive Proxy ('NoMatch a : fields)
_ (a
a, as
as) deps
deps =
    (a
a, forall fieldsProxy node deps.
GHasDependenciesRecursive fieldsProxy node deps =>
fieldsProxy -> node -> deps -> node
genericDependsOnRecursive (forall {k} (t :: k). Proxy t
Proxy :: Proxy fields) as
as deps
deps)

-- Without the kind-signature for '[], ghc will fail to find this
-- instance for nullary constructors
instance GHasDependenciesRecursive (Proxy ('[] :: [Match Type])) () () where
  genericDependsOnRecursive :: Proxy '[] -> () -> () -> ()
genericDependsOnRecursive Proxy '[]
_ ()
_ ()
_ = ()