summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--debian/changelog25
-rw-r--r--doc/todo/use_ghc_8.0_custom_compile_errors.mdwn36
-rw-r--r--propellor.cabal6
-rw-r--r--src/Propellor/EnsureProperty.hs41
-rw-r--r--src/Propellor/PropAccum.hs17
-rw-r--r--src/Propellor/Property/Aiccu.hs5
-rw-r--r--src/Propellor/Property/Atomic.hs12
-rw-r--r--src/Propellor/Property/Systemd.hs1
-rw-r--r--src/Propellor/Property/Tor.hs30
-rw-r--r--src/Propellor/Types.hs36
-rw-r--r--src/Propellor/Types/MetaTypes.hs148
-rw-r--r--stack.yaml3
12 files changed, 101 insertions, 259 deletions
diff --git a/debian/changelog b/debian/changelog
index c74cd929..c263fc96 100644
--- a/debian/changelog
+++ b/debian/changelog
@@ -1,26 +1,5 @@
-propellor (5.9.0) UNRELEASED; urgency=medium
-
- * Avoid displaying an excessive amount of type error messages when many
- properties have been combined in a props list.
- * Added custom type error messages when Properties don't combine due to
- conflicting MetaTypes.
- * Added custom type error messages for ensureProperty and tightenTargets.
- * Note that those changes made ghc 8.0.1 in a few cases unable to infer
- types when ensureProperty or tightenTargets is used. Adding a type
- annotation will work around this problem, if you cannot upgrade
- to a newer ghc that handles them better.
- * Use the type-errors library to detect when the type checker gets stuck
- unable to reduce type-level operations on MetaTypes, and avoid
- displaying massive error messages in such a case.
- * But, since type-errors is a new library not available in eg Debian
- yet, added a WithTypeErrors build flag. When the library is not
- available, cabal will automatically disable that build flag,
- and it will build without the type-errors library.
- * ensureProperty: The constraints have been simplified
- to EnsurePropertyAllowed. (API change)
- * ensureProperty: The contraints have been simplified
- to TightenTargetsAllowed. (API change)
- * CheckCombinable generates a Bool. (API change)
+propellor (5.8.1) UNRELEASED; urgency=medium
+
* Libvirt.installed: install libvirt-daemon-system
Thanks, David Bremner
diff --git a/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn b/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn
index 8c2ed77a..95f86143 100644
--- a/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn
+++ b/doc/todo/use_ghc_8.0_custom_compile_errors.mdwn
@@ -6,25 +6,27 @@ For example, a RevertableProperty is sometimes used where only a regular
Property is accepted. In this case, the error could suggest that the user
apply `setupRevertableProperty` to extract the setup side of the RevertableProperty.
-> I tried this, it didn't seem worth the complication however. --[[Joey]]
-
And, when a Property HasInfo is provided to ensureProperty, propellor could
explain, in the compile error, why it can't let the user do that.
-> Done this and also used custom errors when properties' types don't let
-> them be combined. --[[Joey]]
-
-The new type-errors library builds a lot of stuff on top of this.
-Its ability to detect "stuckness" seems like it may be able to catch
-the very long type errors that we sometimes see when using propellor, and
-whittle them down to a more useful error. --[[Joey]]
-
-> > Actually I think the stuckness would not help with that, though it
-> > could help with other mistakes. In particular, forgetting to provide
-> > a parameter to a property constructor can lead to a massive
-> > error message that leaks type family stuff from MetaTypes, due to
-> > the type checker getting stuck. Detecting that and replacing it with
-> > a simpler error would be a big improvement. Such large error messages
-> > can make ghc use an excessive amount of memory. --[[Joey]]
+Custom errors need a type class to be used. So, could do something like this:
+
+ class NeedsProperty a where
+ withProperty :: (Property metatype -> b) -> b
+
+ instance NeedsProperty (Property metatype) where withProperty = id
+
+ instance TypeError (Text "Use setupRevertableProperty ...")
+ => NeedsProperty RevertableProperty where
+ withProperty = error "unreachable"
+
+(While propellor needs to be buildable with older versions of ghc,
+the `instance TypeError` can just be wrapped in an ifdef to make it only be
+used by the new ghc.)
+
+> The new type-errors library builds a lot of stuff on top of this.
+> Its ability to detect "stuckness" seems like it may be able to catch
+> the very long type errors that we sometimes see when using propellor, and
+> whittle them down to a more useful error. --[[Joey]]
[[!tag user/joey]]
diff --git a/propellor.cabal b/propellor.cabal
index 71d3c578..300313c0 100644
--- a/propellor.cabal
+++ b/propellor.cabal
@@ -35,9 +35,6 @@ Description:
.
It is configured using haskell.
-Flag WithTypeErrors
- Description: Build with type-errors library for better error messages
-
Library
Default-Language: Haskell98
GHC-Options: -Wall -fno-warn-tabs -O0
@@ -50,9 +47,6 @@ Library
directory, filepath, IfElse, process, bytestring, hslogger, split,
unix, unix-compat, ansi-terminal, containers (>= 0.5), network, async,
time, mtl, transformers, exceptions (>= 0.6), stm, text, hashable
- if flag(WithTypeErrors)
- Build-Depends: type-errors
- CPP-Options: -DWITH_TYPE_ERRORS
Exposed-Modules:
Propellor
diff --git a/src/Propellor/EnsureProperty.hs b/src/Propellor/EnsureProperty.hs
index 5ed0325f..ab624706 100644
--- a/src/Propellor/EnsureProperty.hs
+++ b/src/Propellor/EnsureProperty.hs
@@ -8,7 +8,7 @@ module Propellor.EnsureProperty
( ensureProperty
, property'
, OuterMetaTypesWitness
- , EnsurePropertyAllowed
+ , Cannot_ensureProperty_WithInfo
) where
import Propellor.Types
@@ -16,8 +16,6 @@ import Propellor.Types.Core
import Propellor.Types.MetaTypes
import Propellor.Exception
-import GHC.TypeLits
-import Data.Type.Bool
import Data.Monoid
import Prelude
@@ -43,40 +41,19 @@ ensureProperty
-- -Wredundant-constraints is turned off because
-- this constraint appears redundant, but is actually
-- crucial.
- ( EnsurePropertyAllowed inner outer ~ 'True)
+ ( Cannot_ensureProperty_WithInfo inner ~ 'True
+ , (Targets inner `NotSuperset` Targets outer) ~ 'CanCombine
+ )
=> OuterMetaTypesWitness outer
-> Property (MetaTypes inner)
-> Propellor Result
ensureProperty _ = maybe (return NoChange) catchPropellor . getSatisfy
-type family EnsurePropertyAllowed inner outer where
- EnsurePropertyAllowed inner outer =
- (EnsurePropertyNoInfo inner)
- &&
- (EnsurePropertyTargetOSMatches inner outer)
-
-type family EnsurePropertyNoInfo (l :: [a]) :: Bool where
- EnsurePropertyNoInfo '[] = 'True
- EnsurePropertyNoInfo (t ': ts) = If (Not (t `EqT` 'WithInfo))
- (EnsurePropertyNoInfo ts)
- (TypeError ('Text "Cannot use ensureProperty with a Property that HasInfo."))
-
-type family EnsurePropertyTargetOSMatches inner outer where
- EnsurePropertyTargetOSMatches inner outer =
- If (Targets outer `IsSubset` Targets inner)
- 'True
- (IfStuck (Targets outer)
- (TypeError
- ('Text "ensureProperty outer Property type is not able to be inferred here."
- ':$$: 'Text "Consider adding a type annotation."
- )
- )
- (TypeError
- ('Text "ensureProperty inner Property is missing support for: "
- ':$$: PrettyPrintMetaTypes (Difference (Targets outer) (Targets inner))
- )
- )
- )
+-- The name of this was chosen to make type errors a bit more understandable.
+type family Cannot_ensureProperty_WithInfo (l :: [a]) :: Bool where
+ Cannot_ensureProperty_WithInfo '[] = 'True
+ Cannot_ensureProperty_WithInfo (t ': ts) =
+ Not (t `EqT` 'WithInfo) && Cannot_ensureProperty_WithInfo ts
-- | Constructs a property, like `property`, but provides its
-- `OuterMetaTypesWitness`.
diff --git a/src/Propellor/PropAccum.hs b/src/Propellor/PropAccum.hs
index 3fc83202..c60ced73 100644
--- a/src/Propellor/PropAccum.hs
+++ b/src/Propellor/PropAccum.hs
@@ -19,7 +19,6 @@ import Propellor.Types.MetaTypes
import Propellor.Types.Core
import Propellor.Property
-import GHC.TypeLits
import Data.Monoid
import Prelude
@@ -46,16 +45,6 @@ type family GetMetaTypes x where
GetMetaTypes (Property (MetaTypes t)) = MetaTypes t
GetMetaTypes (RevertableProperty (MetaTypes t) undo) = MetaTypes t
--- When many properties are combined, ghc error message
--- can include quite a lot of code, typically starting with
--- `props and including all the properties up to and including the
--- one that fails to combine. Point the user in the right direction.
-type family NoteFor symbol :: ErrorMessage where
- NoteFor symbol =
- 'Text "Probably the problem is with the last property added with "
- ':<>: symbol
- ':<>: 'Text " in the code excerpt below."
-
-- | Adds a property to a Props.
--
-- Can add Properties and RevertableProperties
@@ -66,7 +55,7 @@ type family NoteFor symbol :: ErrorMessage where
-- this constraint appears redundant, but is actually
-- crucial.
, MetaTypes y ~ GetMetaTypes p
- , CheckCombinableNote x y (NoteFor ('Text "&")) ~ 'True
+ , CheckCombinable x y ~ 'CanCombine
)
=> Props (MetaTypes x)
-> p
@@ -81,7 +70,7 @@ Props c & p = Props (c ++ [toChildProperty p])
-- this constraint appears redundant, but is actually
-- crucial.
, MetaTypes y ~ GetMetaTypes p
- , CheckCombinableNote x y (NoteFor ('Text "&^")) ~ 'True
+ , CheckCombinable x y ~ 'CanCombine
)
=> Props (MetaTypes x)
-> p
@@ -93,7 +82,7 @@ Props c &^ p = Props (toChildProperty p : c)
-- -Wredundant-constraints is turned off because
-- this constraint appears redundant, but is actually
-- crucial.
- :: (CheckCombinableNote x z (NoteFor ('Text "!")) ~ 'True)
+ :: (CheckCombinable x z ~ 'CanCombine)
=> Props (MetaTypes x)
-> RevertableProperty (MetaTypes y) (MetaTypes z)
-> Props (MetaTypes (Combine x z))
diff --git a/src/Propellor/Property/Aiccu.hs b/src/Propellor/Property/Aiccu.hs
index 8bf3f283..1b28759c 100644
--- a/src/Propellor/Property/Aiccu.hs
+++ b/src/Propellor/Property/Aiccu.hs
@@ -47,7 +47,8 @@ hasConfig :: TunnelId -> UserName -> Property (HasInfo + DebianLike)
hasConfig t u = prop `onChange` restarted
where
prop :: Property (HasInfo + UnixLike)
- prop = withSomePrivData [(Password (u++"/"++t)), (Password u)] (Context "aiccu") $ \getpassword ->
- property' "aiccu configured" $ \w -> getpassword $ ensureProperty w . go
+ prop = withSomePrivData [(Password (u++"/"++t)), (Password u)] (Context "aiccu") $
+ property' "aiccu configured" . writeConfig
+ writeConfig getpassword w = getpassword $ ensureProperty w . go
go (Password u', p) = confPath `File.hasContentProtected` config u' t p
go (f, _) = error $ "Unexpected type of privdata: " ++ show f
diff --git a/src/Propellor/Property/Atomic.hs b/src/Propellor/Property/Atomic.hs
index 2c7433f6..8519048b 100644
--- a/src/Propellor/Property/Atomic.hs
+++ b/src/Propellor/Property/Atomic.hs
@@ -46,8 +46,10 @@ type CheckAtomicResourcePair a = AtomicResourcePair a -> Propellor (AtomicResour
-- inactiveAtomicResource, and if it was successful,
-- atomically activating that resource.
atomicUpdate
- -- Constriaint inherited from ensureProperty.
- :: (EnsurePropertyAllowed t t ~ 'True)
+ -- Constriaints inherited from ensureProperty.
+ :: ( Cannot_ensureProperty_WithInfo t ~ 'True
+ , (Targets t `NotSuperset` Targets t) ~ 'CanCombine
+ )
=> SingI t
=> AtomicResourcePair a
-> CheckAtomicResourcePair a
@@ -90,8 +92,10 @@ atomicUpdate rbase rcheck rswap mkp = property' d $ \w -> do
-- children: a symlink with the name of the directory itself, and two copies
-- of the directory, with names suffixed with ".1" and ".2"
atomicDirUpdate
- -- Constriaint inherited from ensureProperty.
- :: (EnsurePropertyAllowed t t ~ 'True)
+ -- Constriaints inherited from ensureProperty.
+ :: ( Cannot_ensureProperty_WithInfo t ~ 'True
+ , (Targets t `NotSuperset` Targets t) ~ 'CanCombine
+ )
=> SingI t
=> FilePath
-> (FilePath -> Property (MetaTypes t))
diff --git a/src/Propellor/Property/Systemd.hs b/src/Propellor/Property/Systemd.hs
index 5d597ac6..bfc0f9a5 100644
--- a/src/Propellor/Property/Systemd.hs
+++ b/src/Propellor/Property/Systemd.hs
@@ -391,7 +391,6 @@ mungename = replace "/" "_"
containerCfg :: String -> RevertableProperty (HasInfo + Linux) (HasInfo + Linux)
containerCfg p = RevertableProperty (mk True) (mk False)
where
- mk :: Bool -> Property (HasInfo + Linux)
mk b = tightenTargets $
pureInfoProperty desc $
mempty { _chrootCfg = SystemdNspawnCfg [(p', b)] }
diff --git a/src/Propellor/Property/Tor.hs b/src/Propellor/Property/Tor.hs
index 862af983..426d4209 100644
--- a/src/Propellor/Property/Tor.hs
+++ b/src/Propellor/Property/Tor.hs
@@ -172,22 +172,20 @@ hiddenServiceData hn context = combineProperties desc $ props
where
desc = unwords ["hidden service data available in", varLib </> hn]
installonion :: FilePath -> Property (HasInfo + DebianLike)
- installonion basef =
- let f = varLib </> hn </> basef
- in withPrivData (PrivFile f) context $ \getcontent ->
- property' desc $ \w -> getcontent $ \privcontent ->
- ifM (liftIO $ doesFileExist f)
- ( noChange
- , ensureProperty w $ propertyList desc $ toProps
- [ property desc $ makeChange $ do
- createDirectoryIfMissing True (takeDirectory f)
- writeFileProtected f (unlines (privDataLines privcontent))
- , File.mode (takeDirectory f) $ combineModes
- [ownerReadMode, ownerWriteMode, ownerExecuteMode]
- , File.ownerGroup (takeDirectory f) user (userGroup user)
- , File.ownerGroup f user (userGroup user)
- ]
- )
+ installonion f = withPrivData (PrivFile $ varLib </> hn </> f) context $ \getcontent ->
+ property' desc $ \w -> getcontent $ install w $ varLib </> hn </> f
+ install w f privcontent = ifM (liftIO $ doesFileExist f)
+ ( noChange
+ , ensureProperty w $ propertyList desc $ toProps
+ [ property desc $ makeChange $ do
+ createDirectoryIfMissing True (takeDirectory f)
+ writeFileProtected f (unlines (privDataLines privcontent))
+ , File.mode (takeDirectory f) $ combineModes
+ [ownerReadMode, ownerWriteMode, ownerExecuteMode]
+ , File.ownerGroup (takeDirectory f) user (userGroup user)
+ , File.ownerGroup f user (userGroup user)
+ ]
+ )
restarted :: Property DebianLike
restarted = Service.restarted "tor"
diff --git a/src/Propellor/Types.hs b/src/Propellor/Types.hs
index 026babf0..7052bf92 100644
--- a/src/Propellor/Types.hs
+++ b/src/Propellor/Types.hs
@@ -31,7 +31,6 @@ module Propellor.Types (
, HasInfo
, type (+)
, TightenTargets(..)
- , TightenTargetsAllowed
-- * Combining and modifying properties
, Combines(..)
, CombinedType
@@ -45,8 +44,6 @@ module Propellor.Types (
, module Propellor.Types.ZFS
) where
-import GHC.TypeLits hiding (type (+))
-import Data.Type.Bool
import qualified Data.Semigroup as Sem
import Data.Monoid
import Control.Applicative
@@ -62,7 +59,7 @@ import Propellor.Types.MetaTypes
import Propellor.Types.ZFS
-- | The core data type of Propellor, this represents a property
--- that the system should have, with a description, and an action to ensure
+-- that the system should have, with a descrition, and an action to ensure
-- it has the property.
--
-- There are different types of properties that target different OS's,
@@ -188,17 +185,17 @@ class Combines x y where
-> y
-> CombinedType x y
-instance (CheckCombinable x y ~ 'True, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (Property (MetaTypes y)) where
combineWith f _ (Property _ d1 a1 i1 c1) (Property _ d2 a2 i2 c2) =
Property sing d1 (f a1 a2) i1 (ChildProperty d2 a2 i2 c2 : c1)
-instance (CheckCombinable x y ~ 'True, CheckCombinable x' y' ~ 'True, SingI (Combine x y), SingI (Combine x' y')) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
+instance (CheckCombinable x y ~ 'CanCombine, CheckCombinable x' y' ~ 'CanCombine, SingI (Combine x y), SingI (Combine x' y')) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
combineWith sf tf (RevertableProperty s1 t1) (RevertableProperty s2 t2) =
RevertableProperty
(combineWith sf tf s1 s2)
(combineWith tf sf t1 t2)
-instance (CheckCombinable x y ~ 'True, SingI (Combine x y)) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (RevertableProperty (MetaTypes x) (MetaTypes x')) (Property (MetaTypes y)) where
combineWith sf tf (RevertableProperty x _) y = combineWith sf tf x y
-instance (CheckCombinable x y ~ 'True, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
+instance (CheckCombinable x y ~ 'CanCombine, SingI (Combine x y)) => Combines (Property (MetaTypes x)) (RevertableProperty (MetaTypes y) (MetaTypes y')) where
combineWith sf tf x (RevertableProperty y _) = combineWith sf tf x y
class TightenTargets p where
@@ -212,31 +209,14 @@ class TightenTargets p where
-- > upgraded = tightenTargets $ cmdProperty "apt-get" ["upgrade"]
tightenTargets
::
- ( TightenTargetsAllowed untightened tightened ~ 'True
+ -- Note that this uses PolyKinds
+ ( (Targets untightened `NotSuperset` Targets tightened) ~ 'CanCombine
+ , (NonTargets tightened `NotSuperset` NonTargets untightened) ~ 'CanCombine
, SingI tightened
)
=> p (MetaTypes untightened)
-> p (MetaTypes tightened)
--- Note that this uses PolyKinds
-type family TightenTargetsAllowed untightened tightened where
- TightenTargetsAllowed untightened tightened =
- If (Targets tightened `IsSubset` Targets untightened
- && NonTargets untightened `IsSubset` NonTargets tightened)
- 'True
- (IfStuck (Targets tightened)
- (TypeError
- ('Text "Unable to infer desired Property type in this use of tightenTargets."
- ':$$: ('Text "Consider adding a type annotation.")
- )
- )
- (TypeError
- ('Text "This use of tightenTargets would widen, not narrow, adding: "
- ':$$: PrettyPrintMetaTypes (Difference (Targets tightened) (Targets untightened))
- )
- )
- )
-
instance TightenTargets Property where
tightenTargets (Property _ d a i c) = Property sing d a i c
diff --git a/src/Propellor/Types/MetaTypes.hs b/src/Propellor/Types/MetaTypes.hs
index 567f533a..0c476e87 100644
--- a/src/Propellor/Types/MetaTypes.hs
+++ b/src/Propellor/Types/MetaTypes.hs
@@ -1,5 +1,4 @@
{-# LANGUAGE TypeOperators, PolyKinds, DataKinds, TypeFamilies, UndecidableInstances, FlexibleInstances, GADTs #-}
-{-# LANGUAGE CPP #-}
module Propellor.Types.MetaTypes (
MetaType(..),
@@ -18,33 +17,21 @@ module Propellor.Types.MetaTypes (
IncludesInfo,
Targets,
NonTargets,
- PrettyPrintMetaTypes,
- IsSubset,
+ NotSuperset,
Combine,
+ CheckCombine(..),
CheckCombinable,
- CheckCombinableNote,
type (&&),
Not,
EqT,
Union,
- Intersect,
- Difference,
- IfStuck,
) where
import Propellor.Types.Singletons
import Propellor.Types.OS
-import GHC.TypeLits hiding (type (+))
import Data.Type.Bool
-#ifdef WITH_TYPE_ERRORS
-import Type.Errors
-#else
-type family IfStuck (expr :: k) (b :: k1) (c :: k1) :: k1 where
- IfStuck expr b c = c
-#endif
-
data MetaType
= Targeting TargetOS -- ^ A target OS of a Property
| WithInfo -- ^ Indicates that a Property has associated Info
@@ -126,69 +113,41 @@ type family Combine (list1 :: [a]) (list2 :: [a]) :: [a] where
(Targets list1 `Intersect` Targets list2)
)
--- | Checks if two MetaTypes lists can be safly combined;
--- eg they have at least one Target in common.
-type family IsCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
- -- As a special case, if either list is empty or only WithInfo,
- -- let it be combined with the other. This relies on MetaTypes
- -- list always containing at least one Target, so can only happen
- -- if there's already been a type error. This special case lets the
- -- type checker show only the original type error, and not
- -- subsequent errors due to later CheckCombinable constraints.
- IsCombinable '[] list2 = 'True
- IsCombinable list1 '[] = 'True
- IsCombinable ('WithInfo ': list1) list2 = IsCombinable list1 list2
- IsCombinable list1 ('WithInfo ': list2) = IsCombinable list1 list2
- IsCombinable list1 list2 =
- Not (Null (Combine (Targets list1) (Targets list2)))
-
--- | This (or CheckCombinableNote) should be used anywhere Combine is used,
--- as an additional constraint. For example:
+-- | Checks if two MetaTypes lists can be safely combined.
--
--- > foo :: (CheckCombinable x y ~ 'True) => x -> y -> Combine x y
-type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: Bool where
- CheckCombinable list1 list2 =
- If (IsCombinable list1 list2)
- 'True
- (CannotCombine list1 list2 'Nothing)
-
--- | Allows providing an additional note.
-type family CheckCombinableNote (list1 :: [a]) (list2 :: [a]) (note :: ErrorMessage) :: Bool where
- CheckCombinableNote list1 list2 note =
- If (IsCombinable list1 list2)
- 'True
- (CannotCombine list1 list2
- ('Just ('Text "(" ':<>: note ':<>: 'Text ")"))
- )
-
--- Checking IfStuck is to avoid massive and useless error message leaking
--- type families from this module.
-type family CannotCombine (list1 :: [a]) (list2 :: [a]) (note :: Maybe ErrorMessage) :: Bool where
- CannotCombine list1 list2 note =
- IfStuck list1
- (IfStuck list2
- (TypeError (CannotCombineMessage UnknownType UnknownType UnknownTypeNote))
- (TypeError (CannotCombineMessage UnknownType (PrettyPrintMetaTypes list2) UnknownTypeNote))
- )
- (IfStuck list2
- (TypeError (CannotCombineMessage (PrettyPrintMetaTypes list1) UnknownType UnknownTypeNote))
- (TypeError (CannotCombineMessage (PrettyPrintMetaTypes list1) (PrettyPrintMetaTypes list2) note))
- )
-
-type family UnknownType :: ErrorMessage where
- UnknownType = 'Text "<unknown>"
-
-type family UnknownTypeNote :: Maybe ErrorMessage where
- UnknownTypeNote = 'Just ('Text "(Property <unknown> is often due to a partially applied Property constructor, or due to passing the wrong type to a Property constructor.)")
+-- This should be used anywhere Combine is used, as an additional
+-- constraint. For example:
+--
+-- > foo :: (CheckCombinable x y ~ 'CanCombine) => x -> y -> Combine x y
+type family CheckCombinable (list1 :: [a]) (list2 :: [a]) :: CheckCombine where
+ -- As a special case, if either list is empty, let it be combined
+ -- with the other. This relies on MetaTypes list always containing
+ -- at least one target, so can only happen if there's already been
+ -- a type error. This special case lets the type checker show only
+ -- the original type error, and not an extra error due to a later
+ -- CheckCombinable constraint.
+ CheckCombinable '[] list2 = 'CanCombine
+ CheckCombinable list1 '[] = 'CanCombine
+ CheckCombinable (l1 ': list1) (l2 ': list2) =
+ CheckCombinable' (Combine (l1 ': list1) (l2 ': list2))
+type family CheckCombinable' (combinedlist :: [a]) :: CheckCombine where
+ CheckCombinable' '[] = 'CannotCombineTargets
+ CheckCombinable' (a ': rest)
+ = If (IsTarget a)
+ 'CanCombine
+ (CheckCombinable' rest)
+
+data CheckCombine = CannotCombineTargets | CanCombine
-type family CannotCombineMessage (a :: ErrorMessage) (b :: ErrorMessage) (note :: Maybe ErrorMessage) :: ErrorMessage where
- CannotCombineMessage a b ('Just note) =
- CannotCombineMessage a b 'Nothing
- ':$$: note
- CannotCombineMessage a b 'Nothing =
- 'Text "Cannot combine Properties:"
- ':$$: ('Text " Property " ':<>: a)
- ':$$: ('Text " Property " ':<>: b)
+-- | Every item in the subset must be in the superset.
+--
+-- The name of this was chosen to make type errors more understandable.
+type family NotSuperset (superset :: [a]) (subset :: [a]) :: CheckCombine where
+ NotSuperset superset '[] = 'CanCombine
+ NotSuperset superset (s ': rest) =
+ If (Elem s superset)
+ (NotSuperset superset rest)
+ 'CannotCombineTargets
type family IsTarget (a :: t) :: Bool where
IsTarget ('Targeting a) = 'True
@@ -208,21 +167,6 @@ type family NonTargets (l :: [a]) :: [a] where
(NonTargets xs)
(x ': NonTargets xs)
--- | Pretty-prints a list of MetaTypes for display in a type error message.
-type family PrettyPrintMetaTypes (l :: [MetaType]) :: ErrorMessage where
- PrettyPrintMetaTypes '[] = 'Text "<none>"
- PrettyPrintMetaTypes (t ': '[]) = PrettyPrintMetaType t
- PrettyPrintMetaTypes (t ': ts) =
- PrettyPrintMetaType t ':<>: 'Text " + " ':<>: PrettyPrintMetaTypes ts
-
-type family PrettyPrintMetaType t :: ErrorMessage where
- PrettyPrintMetaType 'WithInfo = 'ShowType HasInfo
- PrettyPrintMetaType ('Targeting 'OSDebian) = 'ShowType Debian
- PrettyPrintMetaType ('Targeting 'OSBuntish) = 'ShowType Buntish
- PrettyPrintMetaType ('Targeting 'OSFreeBSD) = 'ShowType FreeBSD
- PrettyPrintMetaType ('Targeting 'OSArchLinux) = 'ShowType ArchLinux
- PrettyPrintMetaType ('Targeting t) = 'ShowType t
-
-- | Type level elem
type family Elem (a :: t) (list :: [t]) :: Bool where
Elem a '[] = 'False
@@ -244,28 +188,6 @@ type family Intersect (list1 :: [a]) (list2 :: [a]) :: [a] where
(a ': Intersect rest list2)
(Intersect rest list2)
--- | Type level difference. Items that are in the first list, but not in
--- the second.
-type family Difference (list1 :: [a]) (list2 :: [a]) :: [a] where
- Difference '[] list2 = '[]
- Difference (a ': rest) list2 =
- If (Elem a list2)
- (Difference rest list2)
- (a ': Difference rest list2)
-
--- | Every item in the subset must be in the superset.
-type family IsSubset (subset :: [a]) (superset :: [a]) :: Bool where
- IsSubset '[] superset = 'True
- IsSubset (s ': rest) superset =
- If (Elem s superset)
- (IsSubset rest superset)
- 'False
-
--- | Type level null.
-type family Null (list :: [a]) :: Bool where
- Null '[] = 'True
- Null l = 'False
-
-- | Type level equality of metatypes.
type family EqT (a :: MetaType) (b :: MetaType) where
EqT a a = 'True
diff --git a/stack.yaml b/stack.yaml
index 84dbf12e..eb243950 100644
--- a/stack.yaml
+++ b/stack.yaml
@@ -2,6 +2,3 @@
resolver: lts-9.21
packages:
- '.'
-extra-deps:
-- type-errors-0.1.0.0
-- first-class-families-0.5.0.0