{-# 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 :: [Type] where
Inputs (i -> o) = i ': Inputs o
Inputs x = '[]
type family Output f :: Type where
Output (i -> o) = Output o
Output x = x
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
class IsSubset (ins :: [Type]) (out :: [Type]) (target :: Type)
instance IsSubset '[] out t
instance (CanMake a out t, IsSubset els out t) => IsSubset (a ': els) out t
type family Contains (a :: Type) (els :: [Type]) :: Constraint where
Contains a els = Contains1 a els els
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
type (out :- a) = Contains a out
class Solvable (ins :: [Type]) (out :: [Type])
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 :: 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