Update Thyme and improve subsumption of pure and definitely types

data/example/requiring.icicle

···
 -- Only return the result computation
 -- if there was at least `i` facts in
 -- the stream.
-requiring : Aggregate (Definitely Int) -> Aggregate a -> Aggregate (Possibly a)
+requiring : Aggregate Int -> Aggregate a -> Aggregate (Possibly a)
 requiring i x =
-  case (fold x = 0 then x + 1 in x) < i of
+  case count () < i of
     True then
       missing
     False then

icicle-data/src/Icicle/Data/Regex.hs

···
       c' == c
     checkAcceptor c (AcceptRange s fe) =
       c >= s && c <= fe
-    negs neg = if neg then not else id
-
+    negs neg =
+      if neg then not else id
 
     step s0 c =
       let

icicle-data/src/Icicle/Data/Time.hs

···
 {-# LANGUAGE NoImplicitPrelude #-}
 {-# LANGUAGE OverloadedStrings #-}
 {-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE PatternSynonyms   #-}
 module Icicle.Data.Time (
     Date(..)
   , Time(..)
···
 timeOfDays :: Int -> Time
 timeOfDays d
  = Time
- $ flip Thyme.mkUTCTime 0
+ $ flip Thyme.UTCTime 0
  $ Thyme.ModifiedJulianDay d
 
 unsafeTimeOfYMD :: Int -> Int -> Int -> Time
 unsafeTimeOfYMD y m d
  = Time
- $ flip Thyme.mkUTCTime 0
+ $ flip Thyme.UTCTime 0
  $ Thyme.fromGregorian y m d
 
 timeOfYMD :: Int -> Int -> Int -> Maybe Time
 timeOfYMD y m d
  =   Time
- .   flip Thyme.mkUTCTime 0
+ .   flip Thyme.UTCTime 0
  <$> Thyme.fromGregorianValid y m d
 
 timeOfIvorySeconds :: Int64 -> Time
 timeOfIvorySeconds seconds =
-  Time $ Thyme.addUTCTime (fromIntegral seconds) (Thyme.mkUTCTime ivoryEpoch 0)
+  Time $ Thyme.addUTCTime (fromIntegral seconds) (Thyme.UTCTime ivoryEpoch 0)
 
 timeOfYMDHMS :: Int -> Int -> Int -> Int -> Int -> Int -> Time
 timeOfYMDHMS year month day hour minute sec
···
             $ Thyme.TimeOfDay hour minute
             $ Thyme.secondsToDiffTime
             $ fromIntegral sec
-    in Time $ Thyme.mkUTCTime ymd hms
+    in Time $ Thyme.UTCTime ymd hms
 
 -- Unpack the word into an icicle Time
 timeOfPacked :: Word64 -> Time
···
 
 getCurrentDate :: MonadIO m => m Date
 getCurrentDate =
- Date . Thyme.utctDay . Thyme.unUTCTime <$> liftIO Thyme.getCurrentTime
+ Date . Thyme.utctDay <$> liftIO Thyme.getCurrentTime
 
 midnight :: Date -> Time
 midnight (Date date) =
-  Time $ Thyme.mkUTCTime date 0
+  Time $ Thyme.UTCTime date 0
 
 exclusiveSnapshotTime :: Date -> Time
 exclusiveSnapshotTime (Date date) =
-  Time $ Thyme.mkUTCTime (Thyme.addDays 1 date) 0
+  Time $ Thyme.UTCTime (Thyme.addDays 1 date) 0
 
 dateOfYMD :: Int -> Int -> Int -> Maybe Date
 dateOfYMD y m d =
···
 minusDays :: Time -> Int -> Time
 minusDays d i
  = Time
- $ flip Thyme.mkUTCTime (Thyme.utctDayTime view)
+ $ flip Thyme.UTCTime   (Thyme.utctDayTime view)
  $ Thyme.addDays (-i)   (Thyme.utctDay     view)
  where
-   view = getDateTime d ^. Thyme.utcTime
+   view = getDateTime d
 
 minusMonths :: Time -> Int -> Time
 minusMonths d i
  = Time
- $ flip Thyme.mkUTCTime              (Thyme.utctDayTime view)
+ $ flip Thyme.UTCTime                (Thyme.utctDayTime view)
  $ Thyme.addGregorianMonthsClip (-i) (Thyme.utctDay     view)
  where
-   view = getDateTime d ^. Thyme.utcTime
+   view = getDateTime d

icicle-source/src/Icicle/Source/Checker/Function.hs

···
 import                  Icicle.Source.Type
 import                  Icicle.Source.Lexer.Token          (Variable (..))
 
-import                  Icicle.Common.Base
 import qualified        Icicle.Common.Fresh     as Fresh
 
 import                  Icicle.Internal.Pretty (Pretty, pretty)

icicle-source/src/Icicle/Source/Checker/Subsumption.hs

···
      | otherwise
      -> Nothing
 
-    SumT  a1 a2
-     | SumT  b1 b2 <- sig
+    SumT a1 a2
+     | SumT b1 b2 <- sig
      -> join $ combine <$> subsumeT a1 b1 <*> subsumeT a2 b2
      | otherwise
      -> Nothing
 
     StructT as
-     | StructT bs <- sig
+     | StructT bs     <- sig
      , Map.keysSet as == Map.keysSet bs
-     , m' <- Map.intersectionWith (,) as bs
+     , m'             <- Map.intersectionWith (,) as bs
      -> do recordSubs <- traverse (uncurry subsumeT) m'
            foldM combine Map.empty recordSubs
      | otherwise
      -> Nothing
 
+    -- Here we have a special case for pure subsumptions.
+    -- If the temporality is of the inferred site is pure,
+    -- then we accept the unadorned type as the signature.
     Temporality at ar
      | Temporality bt br <- sig
      -> join $ combine <$> subsumeT at bt <*> subsumeT ar br
+     | TemporalityPure <- at
+     -> subsumeT ar sig
      | otherwise
      -> Nothing
 
-    TemporalityPure         -> eq
-    TemporalityElement      -> eq
-    TemporalityAggregate    -> eq
-
+    -- Likewise for possibilities, if the adornment is
+    -- definitely, then the unadorned type is fine.
     Possibility at ar
      | Possibility bt br <- sig
      -> join $ combine <$> subsumeT at bt <*> subsumeT ar br
+     | PossibilityDefinitely <- at
+     -> subsumeT ar sig
      | otherwise
      -> Nothing
 
-    PossibilityPossibly     -> eq
+    TemporalityPure         -> eq
+    TemporalityElement      -> eq
+    TemporalityAggregate    -> eq
+
     PossibilityDefinitely   -> eq
+    PossibilityPossibly     -> eq
 
     TypeArrow at ar
      | TypeArrow bt br <- sig