{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE UndecidableInstances #-}
{-# OPTIONS_GHC -fno-warn-unticked-promoted-constructors #-}
module Data.Registry.Solver where
import Data.Kind
import GHC.TypeLits
type family Inputs f :: [*] where
Inputs (i -> o) = i ': Inputs o
Inputs x = '[]
type family Output f :: * where
Output (i -> o) = Output o
Output x = x
type family Contains (a :: *) (els :: [*]) :: Constraint where
Contains a '[] = TypeError (Text "No element of type " ':<>: 'ShowType a ':<>: 'Text " can be built out of the registry")
Contains a (a ': els) = ()
Contains a (b ': els) = Contains a els
type (out :- a) = Contains a out
class IsSubset (ins :: [*]) (out :: [*])
instance IsSubset '[] out
instance (Contains a out, IsSubset els out) => IsSubset (a ': els) out
class Solvable (ins :: [*]) (out :: [*])
instance (IsSubset ins out) => Solvable ins out
type family (:++) (x :: [k]) (y :: [k]) :: [k] where
'[] :++ xs = xs
(x ': xs) :++ ys = x ': (xs :++ ys)
type family FindUnique (a :: *) (as :: [*]) :: [*] where
FindUnique a '[] = '[a]
FindUnique a (a ': rest) = '[]
FindUnique a (b ': rest) = FindUnique a rest
type family Normalized (as :: [*]) :: [*] where
Normalized '[] = '[]
Normalized '[a] = '[a]
Normalized (a ': rest) = FindUnique a rest :++ Normalized rest