{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}

-- |
--  Type level functions to statically assess
--  if a value can be built out of a Registry
module Data.Registry.Solver where

import Data.Kind
import GHC.TypeLits

-- | Compute the list of input types for a function
type family Inputs f :: [Type] where
  Inputs (i -> o) = i ': Inputs o
  Inputs x = '[]

-- | Compute the output type for a function
type family Output f :: Type where
  Output (i -> o) = Output o
  Output x = x

-- | Compute if a constructor can be added to a registry
type family CanMake (a :: Type) (els :: [Type]) (target :: Type) :: Constraint where
  CanMake a '[] t =
    TypeError
      ( Text "The constructor for "
          :$$: Text ""
          :$$: (Text "  " :<>: ShowType (Output t))
          :$$: Text ""
          :$$: Text "cannot be added to the registry because"
          :$$: Text ""
          :$$: (Text "  " :<>: ShowType (Output a))
          :$$: Text ""
          :$$: Text " is not one of the registry outputs"
          :$$: Text ""
          :$$: (Text "The full constructor type for " :<>: ShowType (Output t) :<>: Text " is")
          :$$: Text ""
          :$$: ShowType t
          :$$: Text ""
      )
  CanMake a (a ': _els) _t = ()
  CanMake a (_b ': els) t = CanMake a els t

-- | Compute if each element of a list of types is contained in
-- another list
class IsSubset (ins :: [Type]) (out :: [Type]) (target :: Type)

instance IsSubset '[] out t

-- | The list of elements: a + els is a subset of out if els is a subset of out and
--   a is also included in the set out. The search for a in out is done via a
--   type family in order to be able to display an error message if it can't be found
instance (CanMake a out t, IsSubset els out t) => IsSubset (a ': els) out t

-- | Compute if each element of a list of types
--   is the same as another in a different order
class IsSameSet (types1 :: [Type]) (types2 :: [Type])

instance (ts1 ~ Normalized types1, ts2 ~ Normalized types2, IsSubset ts1 ts2 (), IsSubset ts1 ts2 ()) => IsSameSet types1 types2

-- | Compute if a type is contained in a list of types
type family Contains (a :: Type) (els :: [Type]) :: Constraint where
  Contains a els = Contains1 a els els

-- | Compute if a type is contained in a list of types
type family Contains1 (a :: Type) (els :: [Type]) (target :: [Type]) :: Constraint where
  Contains1 a '[] target = TypeError ('ShowType a ':<>: Text " cannot be found in " ':<>: 'ShowType target)
  Contains1 a (a ': els) t = ()
  Contains1 a (b ': els) t = Contains1 a els t

-- | Shorthand type alias when many such constraints need to be added to a type signature
type out :- a = Contains a out

-- | From the list of all the input types and outputs types of a registry
--   Can we create all the output types?
class Solvable (ins :: [Type]) (out :: [Type])

instance (IsSubset ins out ()) => Solvable ins out

-- | Extracted from the typelevel-sets project and adapted for the Registry datatype
--   This union deduplicates elements only if they appear in contiguously
--   What we really want is typelevel sets but they are too slow for now
--   https://github.com/dorchard/type-level-sets/issues/17
type family (:++) (x :: [k]) (y :: [k]) :: [k] where
  '[] :++ xs = xs
  (x ': xs) :++ ys = x ': (xs :++ ys)

-- | Return '[a] only if it is not already in the list of types
type family FindUnique (a :: Type) (as :: [Type]) :: [Type] where
  FindUnique a '[] = '[a]
  FindUnique a (a ': _rest) = '[]
  FindUnique a (_b ': rest) = FindUnique a rest

type family Normalized (as :: [Type]) :: [Type] where
  Normalized '[] = '[]
  Normalized '[a] = '[a]
  Normalized (a ': rest) = FindUnique a rest :++ Normalized rest