From 61a1ba8ff1fa496af24d22986057a7607ae55ff1 Mon Sep 17 00:00:00 2001 From: Joey Hess Date: Tue, 8 Mar 2016 17:54:49 -0400 Subject: make it a type error to intersect two OS lists if the result is empty --- doc/todo/type_level_OS_requirements.mdwn | 4 +++- src/Propellor/Types/OS/Typelevel.hs | 15 +++++++++++---- 2 files changed, 14 insertions(+), 5 deletions(-) diff --git a/doc/todo/type_level_OS_requirements.mdwn b/doc/todo/type_level_OS_requirements.mdwn index 65e6099f..6d5d7aaf 100644 --- a/doc/todo/type_level_OS_requirements.mdwn +++ b/doc/todo/type_level_OS_requirements.mdwn @@ -11,7 +11,9 @@ For example, `Property i '[Debian, FreeBSD]` combined with `Property i '[Debian, yields a `Property i '[Debian]` -- the intersection of the OS's supported by the combined properties. -And, combining two properties that demand different OS's would need to be a +Combining two properties that demand different OS's would yield a +`Property i '[]` -- since the type level OS list is empty, + type error. Can a type level function combine two types successfully, and fail to combine two others somehow? Don't know. Maybe combine to an IncoherentOS and don't allow a `Property i IncoherentOS` to be used in a diff --git a/src/Propellor/Types/OS/Typelevel.hs b/src/Propellor/Types/OS/Typelevel.hs index 82f3a426..879259df 100644 --- a/src/Propellor/Types/OS/Typelevel.hs +++ b/src/Propellor/Types/OS/Typelevel.hs @@ -43,9 +43,8 @@ freeBSD = typeOS OSFreeBSD typeOS :: SupportedOS -> OSList os typeOS o = OSList [o] --- FIXME, should type check --- foo :: OSList '[OSDebian, OSFreeBSD] --- foo = (debian `combineSupportedOS` freeBSD ) `intersectSupportedOS` unixlike +foo :: OSList '[OSDebian, OSFreeBSD] +foo = (debian `combineSupportedOS` freeBSD ) `intersectSupportedOS` unixlike -- | Combines two lists of supported OS's, yielding a list with the -- contents of both. @@ -63,12 +62,20 @@ type instance ConcatOSList (a ': rest) list2 = a ': ConcatOSList rest list2 -- | The intersection between two lists of supported OS's. intersectSupportedOS - :: (r ~ IntersectOSList l1 l2) + :: (r ~ IntersectOSList l1 l2, CannotCombineOS l1 l2 r ~ CanCombineOS) => OSList l1 -> OSList l2 -> OSList r intersectSupportedOS (OSList l1) (OSList l2) = OSList (filter (`elem` l2) l1) +-- | Detect intersection of two lists that don't have any common OS. +-- +-- The name of this was chosen to make type errors a more understandable. +type family CannotCombineOS (list1 :: [a]) (list2 :: [a]) (listr :: [a]) :: CheckIntersection +type instance CannotCombineOS l1 l2 '[] = 'CannotCombineOS +type instance CannotCombineOS l1 l2 (a ': rest) = 'CanCombineOS +data CheckIntersection = CannotCombineOS | CanCombineOS + -- | Type level intersection for OSList type family IntersectOSList (list1 :: [a]) (list2 :: [a]) :: [a] type instance IntersectOSList '[] list2 = '[] -- cgit v1.2.3