summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--doc/todo/type_level_OS_requirements.mdwn4
-rw-r--r--src/Propellor/Types/OS/Typelevel.hs15
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 = '[]