    -- | Syntax of size expressions and constraints.

    module Agda.TypeChecking.SizedTypes.Syntax where

    import Prelude hiding ( null )

    import Data.Map (Map)
    import qualified Data.Map as Map
    import Data.Set (Set)
    import qualified Data.Set as Set

    import Agda.TypeChecking.SizedTypes.Utils

    import Agda.Utils.Functor
    import Agda.Utils.Null
    import Agda.Utils.Pretty

    import Agda.Utils.Impossible

    -- * Syntax

    -- | Constant finite sizes @n >= 0@.
    newtype Offset = O Int
      deriving (Offset -> Offset -> Bool
    (Offset -> Offset -> Bool)
    -> (Offset -> Offset -> Bool) -> Eq Offset
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Offset -> Offset -> Bool
    $c/= :: Offset -> Offset -> Bool
    == :: Offset -> Offset -> Bool
    $c== :: Offset -> Offset -> Bool
    Eq, Eq Offset
    Eq Offset
    -> (Offset -> Offset -> Ordering)
    -> (Offset -> Offset -> Bool)
    -> (Offset -> Offset -> Bool)
    -> (Offset -> Offset -> Bool)
    -> (Offset -> Offset -> Bool)
    -> (Offset -> Offset -> Offset)
    -> (Offset -> Offset -> Offset)
    -> Ord Offset
    Offset -> Offset -> Bool
    Offset -> Offset -> Ordering
    Offset -> Offset -> Offset
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Offset -> Offset -> Offset
    $cmin :: Offset -> Offset -> Offset
    max :: Offset -> Offset -> Offset
    $cmax :: Offset -> Offset -> Offset
    >= :: Offset -> Offset -> Bool
    $c>= :: Offset -> Offset -> Bool
    > :: Offset -> Offset -> Bool
    $c> :: Offset -> Offset -> Bool
    <= :: Offset -> Offset -> Bool
    $c<= :: Offset -> Offset -> Bool
    < :: Offset -> Offset -> Bool
    $c< :: Offset -> Offset -> Bool
    compare :: Offset -> Offset -> Ordering
    $ccompare :: Offset -> Offset -> Ordering
    Ord, Integer -> Offset
    Offset -> Offset
    Offset -> Offset -> Offset
    (Offset -> Offset -> Offset)
    -> (Offset -> Offset -> Offset)
    -> (Offset -> Offset -> Offset)
    -> (Offset -> Offset)
    -> (Offset -> Offset)
    -> (Offset -> Offset)
    -> (Integer -> Offset)
    -> Num Offset
    forall a.
    (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (a -> a)
    -> (Integer -> a)
    -> Num a
    fromInteger :: Integer -> Offset
    $cfromInteger :: Integer -> Offset
    signum :: Offset -> Offset
    $csignum :: Offset -> Offset
    abs :: Offset -> Offset
    $cabs :: Offset -> Offset
    negate :: Offset -> Offset
    $cnegate :: Offset -> Offset
    * :: Offset -> Offset -> Offset
    $c* :: Offset -> Offset -> Offset
    - :: Offset -> Offset -> Offset
    $c- :: Offset -> Offset -> Offset
    + :: Offset -> Offset -> Offset
    $c+ :: Offset -> Offset -> Offset
    Num, Int -> Offset
    Offset -> Int
    Offset -> [Offset]
    Offset -> Offset
    Offset -> Offset -> [Offset]
    Offset -> Offset -> Offset -> [Offset]
    (Offset -> Offset)
    -> (Offset -> Offset)
    -> (Int -> Offset)
    -> (Offset -> Int)
    -> (Offset -> [Offset])
    -> (Offset -> Offset -> [Offset])
    -> (Offset -> Offset -> [Offset])
    -> (Offset -> Offset -> Offset -> [Offset])
    -> Enum Offset
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
    $cenumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
    enumFromTo :: Offset -> Offset -> [Offset]
    $cenumFromTo :: Offset -> Offset -> [Offset]
    enumFromThen :: Offset -> Offset -> [Offset]
    $cenumFromThen :: Offset -> Offset -> [Offset]
    enumFrom :: Offset -> [Offset]
    $cenumFrom :: Offset -> [Offset]
    fromEnum :: Offset -> Int
    $cfromEnum :: Offset -> Int
    toEnum :: Int -> Offset
    $ctoEnum :: Int -> Offset
    pred :: Offset -> Offset
    $cpred :: Offset -> Offset
    succ :: Offset -> Offset
    $csucc :: Offset -> Offset
    Enum)

    -- This Show instance is ok because of the Num constraint.
    instance Show Offset where
      show :: Offset -> String
    show (O Int
    n) = Int -> String
    forall a. Show a => a -> String
    show Int
    n

    instance Pretty Offset where
      pretty :: Offset -> Doc
    pretty (O Int
    n) = Int -> Doc
    forall a. Pretty a => a -> Doc
    pretty Int
    n

    instance MeetSemiLattice Offset where
      meet :: Offset -> Offset -> Offset
    meet = Offset -> Offset -> Offset
    forall a. Ord a => a -> a -> a
    min

    instance Plus Offset Offset Offset where
      plus :: Offset -> Offset -> Offset
    plus (O Int
    x) (O Int
    y) = Int -> Offset
    O (Int -> Int -> Int
    forall a b c. Plus a b c => a -> b -> c
    plus Int
    x Int
    y)

    -- | Fixed size variables @i@.
    newtype Rigid  = RigidId { Rigid -> String
    rigidId :: String }
      deriving (Rigid -> Rigid -> Bool
    (Rigid -> Rigid -> Bool) -> (Rigid -> Rigid -> Bool) -> Eq Rigid
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Rigid -> Rigid -> Bool
    $c/= :: Rigid -> Rigid -> Bool
    == :: Rigid -> Rigid -> Bool
    $c== :: Rigid -> Rigid -> Bool
    Eq, Eq Rigid
    Eq Rigid
    -> (Rigid -> Rigid -> Ordering)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Bool)
    -> (Rigid -> Rigid -> Rigid)
    -> (Rigid -> Rigid -> Rigid)
    -> Ord Rigid
    Rigid -> Rigid -> Bool
    Rigid -> Rigid -> Ordering
    Rigid -> Rigid -> Rigid
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Rigid -> Rigid -> Rigid
    $cmin :: Rigid -> Rigid -> Rigid
    max :: Rigid -> Rigid -> Rigid
    $cmax :: Rigid -> Rigid -> Rigid
    >= :: Rigid -> Rigid -> Bool
    $c>= :: Rigid -> Rigid -> Bool
    > :: Rigid -> Rigid -> Bool
    $c> :: Rigid -> Rigid -> Bool
    <= :: Rigid -> Rigid -> Bool
    $c<= :: Rigid -> Rigid -> Bool
    < :: Rigid -> Rigid -> Bool
    $c< :: Rigid -> Rigid -> Bool
    compare :: Rigid -> Rigid -> Ordering
    $ccompare :: Rigid -> Rigid -> Ordering
    Ord)

    instance Show Rigid where
      show :: Rigid -> String
    show (RigidId String
    s) = String
    "RigidId " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s

    instance Pretty Rigid where
      pretty :: Rigid -> Doc
    pretty = String -> Doc
    text (String -> Doc) -> (Rigid -> String) -> Rigid -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Rigid -> String
    rigidId

    -- | Size meta variables @X@ to solve for.
    newtype Flex   = FlexId { Flex -> String
    flexId :: String }
      deriving (Flex -> Flex -> Bool
    (Flex -> Flex -> Bool) -> (Flex -> Flex -> Bool) -> Eq Flex
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Flex -> Flex -> Bool
    $c/= :: Flex -> Flex -> Bool
    == :: Flex -> Flex -> Bool
    $c== :: Flex -> Flex -> Bool
    Eq, Eq Flex
    Eq Flex
    -> (Flex -> Flex -> Ordering)
    -> (Flex -> Flex -> Bool)
    -> (Flex -> Flex -> Bool)
    -> (Flex -> Flex -> Bool)
    -> (Flex -> Flex -> Bool)
    -> (Flex -> Flex -> Flex)
    -> (Flex -> Flex -> Flex)
    -> Ord Flex
    Flex -> Flex -> Bool
    Flex -> Flex -> Ordering
    Flex -> Flex -> Flex
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Flex -> Flex -> Flex
    $cmin :: Flex -> Flex -> Flex
    max :: Flex -> Flex -> Flex
    $cmax :: Flex -> Flex -> Flex
    >= :: Flex -> Flex -> Bool
    $c>= :: Flex -> Flex -> Bool
    > :: Flex -> Flex -> Bool
    $c> :: Flex -> Flex -> Bool
    <= :: Flex -> Flex -> Bool
    $c<= :: Flex -> Flex -> Bool
    < :: Flex -> Flex -> Bool
    $c< :: Flex -> Flex -> Bool
    compare :: Flex -> Flex -> Ordering
    $ccompare :: Flex -> Flex -> Ordering
    Ord)

    instance Show Flex where
      show :: Flex -> String
    show (FlexId String
    s) = String
    "FlexId " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ ShowS
    forall a. Show a => a -> String
    show String
    s

    instance Pretty Flex where
      pretty :: Flex -> Doc
    pretty = String -> Doc
    text (String -> Doc) -> (Flex -> String) -> Flex -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Flex -> String
    flexId

    -- | Size expressions appearing in constraints.
    data SizeExpr' rigid flex
      = Const { forall rigid flex. SizeExpr' rigid flex -> Offset
    offset :: Offset }                   -- ^ Constant number @n@.
      | Rigid { forall rigid flex. SizeExpr' rigid flex -> rigid
    rigid  :: rigid, offset :: Offset }  -- ^ Variable plus offset @i + n@.
      | Infty                                        -- ^ Infinity @∞@.
      | Flex  { forall rigid flex. SizeExpr' rigid flex -> flex
    flex   :: flex, offset :: Offset }   -- ^ Meta variable @X + n@.
        deriving (Int -> SizeExpr' rigid flex -> ShowS
    [SizeExpr' rigid flex] -> ShowS
    SizeExpr' rigid flex -> String
    (Int -> SizeExpr' rigid flex -> ShowS)
    -> (SizeExpr' rigid flex -> String)
    -> ([SizeExpr' rigid flex] -> ShowS)
    -> Show (SizeExpr' rigid flex)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> SizeExpr' rigid flex -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    [SizeExpr' rigid flex] -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    SizeExpr' rigid flex -> String
    showList :: [SizeExpr' rigid flex] -> ShowS
    $cshowList :: forall rigid flex.
    (Show rigid, Show flex) =>
    [SizeExpr' rigid flex] -> ShowS
    show :: SizeExpr' rigid flex -> String
    $cshow :: forall rigid flex.
    (Show rigid, Show flex) =>
    SizeExpr' rigid flex -> String
    showsPrec :: Int -> SizeExpr' rigid flex -> ShowS
    $cshowsPrec :: forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> SizeExpr' rigid flex -> ShowS
    Show, SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> Eq (SizeExpr' rigid flex)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall rigid flex.
    (Eq rigid, Eq flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    /= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c/= :: forall rigid flex.
    (Eq rigid, Eq flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    == :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c== :: forall rigid flex.
    (Eq rigid, Eq flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    Eq, Eq (SizeExpr' rigid flex)
    Eq (SizeExpr' rigid flex)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> (SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool)
    -> (SizeExpr' rigid flex
        -> SizeExpr' rigid flex -> SizeExpr' rigid flex)
    -> (SizeExpr' rigid flex
        -> SizeExpr' rigid flex -> SizeExpr' rigid flex)
    -> Ord (SizeExpr' rigid flex)
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    forall {rigid} {flex}.
    (Ord rigid, Ord flex) =>
    Eq (SizeExpr' rigid flex)
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    min :: SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    $cmin :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    max :: SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    $cmax :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex
    -> SizeExpr' rigid flex -> SizeExpr' rigid flex
    >= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c>= :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    > :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c> :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    <= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c<= :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    < :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $c< :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    $ccompare :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    Ord, (forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b)
    -> (forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a)
    -> Functor (SizeExpr' rigid)
    forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    forall rigid a b.
    (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    $c<$ :: forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    fmap :: forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    $cfmap :: forall rigid a b.
    (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    Functor, (forall m. Monoid m => SizeExpr' rigid m -> m)
    -> (forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m)
    -> (forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m)
    -> (forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b)
    -> (forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b)
    -> (forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b)
    -> (forall a. (a -> a -> a) -> SizeExpr' rigid a -> a)
    -> (forall a. (a -> a -> a) -> SizeExpr' rigid a -> a)
    -> (forall a. SizeExpr' rigid a -> [a])
    -> (forall a. SizeExpr' rigid a -> Bool)
    -> (forall a. SizeExpr' rigid a -> Int)
    -> (forall a. Eq a => a -> SizeExpr' rigid a -> Bool)
    -> (forall a. Ord a => SizeExpr' rigid a -> a)
    -> (forall a. Ord a => SizeExpr' rigid a -> a)
    -> (forall a. Num a => SizeExpr' rigid a -> a)
    -> (forall a. Num a => SizeExpr' rigid a -> a)
    -> Foldable (SizeExpr' rigid)
    forall a. Eq a => a -> SizeExpr' rigid a -> Bool
    forall a. Num a => SizeExpr' rigid a -> a
    forall a. Ord a => SizeExpr' rigid a -> a
    forall m. Monoid m => SizeExpr' rigid m -> m
    forall a. SizeExpr' rigid a -> Bool
    forall a. SizeExpr' rigid a -> Int
    forall a. SizeExpr' rigid a -> [a]
    forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
    forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
    forall rigid a. Num a => SizeExpr' rigid a -> a
    forall rigid a. Ord a => SizeExpr' rigid a -> a
    forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    forall rigid m. Monoid m => SizeExpr' rigid m -> m
    forall rigid a. SizeExpr' rigid a -> Bool
    forall rigid a. SizeExpr' rigid a -> Int
    forall rigid a. SizeExpr' rigid a -> [a]
    forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
    forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => SizeExpr' rigid a -> a
    $cproduct :: forall rigid a. Num a => SizeExpr' rigid a -> a
    sum :: forall a. Num a => SizeExpr' rigid a -> a
    $csum :: forall rigid a. Num a => SizeExpr' rigid a -> a
    minimum :: forall a. Ord a => SizeExpr' rigid a -> a
    $cminimum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
    maximum :: forall a. Ord a => SizeExpr' rigid a -> a
    $cmaximum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
    elem :: forall a. Eq a => a -> SizeExpr' rigid a -> Bool
    $celem :: forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
    length :: forall a. SizeExpr' rigid a -> Int
    $clength :: forall rigid a. SizeExpr' rigid a -> Int
    null :: forall a. SizeExpr' rigid a -> Bool
    $cnull :: forall rigid a. SizeExpr' rigid a -> Bool
    toList :: forall a. SizeExpr' rigid a -> [a]
    $ctoList :: forall rigid a. SizeExpr' rigid a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
    $cfoldl1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
    foldr1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
    $cfoldr1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    $cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    $cfoldl :: forall rigid b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    $cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    $cfoldr :: forall rigid a b. (a -> b -> b) -> b -> SizeExpr' rigid a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    $cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    $cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    fold :: forall m. Monoid m => SizeExpr' rigid m -> m
    $cfold :: forall rigid m. Monoid m => SizeExpr' rigid m -> m
    Foldable, Functor (SizeExpr' rigid)
    Foldable (SizeExpr' rigid)
    Functor (SizeExpr' rigid)
    -> Foldable (SizeExpr' rigid)
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        SizeExpr' rigid (f a) -> f (SizeExpr' rigid a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        SizeExpr' rigid (m a) -> m (SizeExpr' rigid a))
    -> Traversable (SizeExpr' rigid)
    forall rigid. Functor (SizeExpr' rigid)
    forall rigid. Foldable (SizeExpr' rigid)
    forall rigid (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    forall rigid (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    forall (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    $csequence :: forall rigid (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    $cmapM :: forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    $csequenceA :: forall rigid (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    $ctraverse :: forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    Traversable)

    type SizeExpr = SizeExpr' Rigid Flex

    -- | Comparison operator, e.g. for size expression.
    data Cmp
      = Lt  -- ^ @<@.
      | Le  -- ^ @≤@.
      deriving (Int -> Cmp -> ShowS
    [Cmp] -> ShowS
    Cmp -> String
    (Int -> Cmp -> ShowS)
    -> (Cmp -> String) -> ([Cmp] -> ShowS) -> Show Cmp
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    showList :: [Cmp] -> ShowS
    $cshowList :: [Cmp] -> ShowS
    show :: Cmp -> String
    $cshow :: Cmp -> String
    showsPrec :: Int -> Cmp -> ShowS
    $cshowsPrec :: Int -> Cmp -> ShowS
    Show, Cmp -> Cmp -> Bool
    (Cmp -> Cmp -> Bool) -> (Cmp -> Cmp -> Bool) -> Eq Cmp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Cmp -> Cmp -> Bool
    $c/= :: Cmp -> Cmp -> Bool
    == :: Cmp -> Cmp -> Bool
    $c== :: Cmp -> Cmp -> Bool
    Eq, Cmp
    Cmp -> Cmp -> Bounded Cmp
    forall a. a -> a -> Bounded a
    maxBound :: Cmp
    $cmaxBound :: Cmp
    minBound :: Cmp
    $cminBound :: Cmp
    Bounded, Int -> Cmp
    Cmp -> Int
    Cmp -> [Cmp]
    Cmp -> Cmp
    Cmp -> Cmp -> [Cmp]
    Cmp -> Cmp -> Cmp -> [Cmp]
    (Cmp -> Cmp)
    -> (Cmp -> Cmp)
    -> (Int -> Cmp)
    -> (Cmp -> Int)
    -> (Cmp -> [Cmp])
    -> (Cmp -> Cmp -> [Cmp])
    -> (Cmp -> Cmp -> [Cmp])
    -> (Cmp -> Cmp -> Cmp -> [Cmp])
    -> Enum Cmp
    forall a.
    (a -> a)
    -> (a -> a)
    -> (Int -> a)
    -> (a -> Int)
    -> (a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> [a])
    -> (a -> a -> a -> [a])
    -> Enum a
    enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
    $cenumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
    enumFromTo :: Cmp -> Cmp -> [Cmp]
    $cenumFromTo :: Cmp -> Cmp -> [Cmp]
    enumFromThen :: Cmp -> Cmp -> [Cmp]
    $cenumFromThen :: Cmp -> Cmp -> [Cmp]
    enumFrom :: Cmp -> [Cmp]
    $cenumFrom :: Cmp -> [Cmp]
    fromEnum :: Cmp -> Int
    $cfromEnum :: Cmp -> Int
    toEnum :: Int -> Cmp
    $ctoEnum :: Int -> Cmp
    pred :: Cmp -> Cmp
    $cpred :: Cmp -> Cmp
    succ :: Cmp -> Cmp
    $csucc :: Cmp -> Cmp
    Enum)

    instance Dioid Cmp where
      compose :: Cmp -> Cmp -> Cmp
    compose     = Cmp -> Cmp -> Cmp
    forall a. Ord a => a -> a -> a
    min
      unitCompose :: Cmp
    unitCompose = Cmp
    Le

    -- | Comparison operator is ordered @'Lt' < 'Le'@.
    instance Ord Cmp where
      Cmp
    Lt <= :: Cmp -> Cmp -> Bool
    <= Cmp
    x  = Bool
    True
      Cmp
    Le <= Cmp
    Lt = Bool
    False
      Cmp
    Le <= Cmp
    Le = Bool
    True

    instance MeetSemiLattice Cmp where
      meet :: Cmp -> Cmp -> Cmp
    meet = Cmp -> Cmp -> Cmp
    forall a. Ord a => a -> a -> a
    min

    instance Top Cmp where
      top :: Cmp
    top = Cmp
    Le

    -- | Constraint: an inequation between size expressions,
    --   e.g. @X < ∞@ or @i + 3 ≤ j@.
    data Constraint' rigid flex = Constraint
      { forall rigid flex. Constraint' rigid flex -> SizeExpr' rigid flex
    leftExpr  :: SizeExpr' rigid flex
      , forall rigid flex. Constraint' rigid flex -> Cmp
    cmp       :: Cmp
      , forall rigid flex. Constraint' rigid flex -> SizeExpr' rigid flex
    rightExpr :: SizeExpr' rigid flex
      }
      deriving (Int -> Constraint' rigid flex -> ShowS
    [Constraint' rigid flex] -> ShowS
    Constraint' rigid flex -> String
    (Int -> Constraint' rigid flex -> ShowS)
    -> (Constraint' rigid flex -> String)
    -> ([Constraint' rigid flex] -> ShowS)
    -> Show (Constraint' rigid flex)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> Constraint' rigid flex -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    [Constraint' rigid flex] -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    Constraint' rigid flex -> String
    showList :: [Constraint' rigid flex] -> ShowS
    $cshowList :: forall rigid flex.
    (Show rigid, Show flex) =>
    [Constraint' rigid flex] -> ShowS
    show :: Constraint' rigid flex -> String
    $cshow :: forall rigid flex.
    (Show rigid, Show flex) =>
    Constraint' rigid flex -> String
    showsPrec :: Int -> Constraint' rigid flex -> ShowS
    $cshowsPrec :: forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> Constraint' rigid flex -> ShowS
    Show, (forall a b.
     (a -> b) -> Constraint' rigid a -> Constraint' rigid b)
    -> (forall a b. a -> Constraint' rigid b -> Constraint' rigid a)
    -> Functor (Constraint' rigid)
    forall a b. a -> Constraint' rigid b -> Constraint' rigid a
    forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
    forall rigid a b.
    (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    <$ :: forall a b. a -> Constraint' rigid b -> Constraint' rigid a
    $c<$ :: forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
    fmap :: forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    $cfmap :: forall rigid a b.
    (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    Functor, (forall m. Monoid m => Constraint' rigid m -> m)
    -> (forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m)
    -> (forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m)
    -> (forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b)
    -> (forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b)
    -> (forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b)
    -> (forall a. (a -> a -> a) -> Constraint' rigid a -> a)
    -> (forall a. (a -> a -> a) -> Constraint' rigid a -> a)
    -> (forall a. Constraint' rigid a -> [a])
    -> (forall a. Constraint' rigid a -> Bool)
    -> (forall a. Constraint' rigid a -> Int)
    -> (forall a. Eq a => a -> Constraint' rigid a -> Bool)
    -> (forall a. Ord a => Constraint' rigid a -> a)
    -> (forall a. Ord a => Constraint' rigid a -> a)
    -> (forall a. Num a => Constraint' rigid a -> a)
    -> (forall a. Num a => Constraint' rigid a -> a)
    -> Foldable (Constraint' rigid)
    forall a. Eq a => a -> Constraint' rigid a -> Bool
    forall a. Num a => Constraint' rigid a -> a
    forall a. Ord a => Constraint' rigid a -> a
    forall m. Monoid m => Constraint' rigid m -> m
    forall a. Constraint' rigid a -> Bool
    forall a. Constraint' rigid a -> Int
    forall a. Constraint' rigid a -> [a]
    forall a. (a -> a -> a) -> Constraint' rigid a -> a
    forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
    forall rigid a. Num a => Constraint' rigid a -> a
    forall rigid a. Ord a => Constraint' rigid a -> a
    forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    forall rigid m. Monoid m => Constraint' rigid m -> m
    forall rigid a. Constraint' rigid a -> Bool
    forall rigid a. Constraint' rigid a -> Int
    forall rigid a. Constraint' rigid a -> [a]
    forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
    forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    forall (t :: * -> *).
    (forall m. Monoid m => t m -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall m a. Monoid m => (a -> m) -> t a -> m)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall a b. (a -> b -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall b a. (b -> a -> b) -> b -> t a -> b)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. (a -> a -> a) -> t a -> a)
    -> (forall a. t a -> [a])
    -> (forall a. t a -> Bool)
    -> (forall a. t a -> Int)
    -> (forall a. Eq a => a -> t a -> Bool)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Ord a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> (forall a. Num a => t a -> a)
    -> Foldable t
    product :: forall a. Num a => Constraint' rigid a -> a
    $cproduct :: forall rigid a. Num a => Constraint' rigid a -> a
    sum :: forall a. Num a => Constraint' rigid a -> a
    $csum :: forall rigid a. Num a => Constraint' rigid a -> a
    minimum :: forall a. Ord a => Constraint' rigid a -> a
    $cminimum :: forall rigid a. Ord a => Constraint' rigid a -> a
    maximum :: forall a. Ord a => Constraint' rigid a -> a
    $cmaximum :: forall rigid a. Ord a => Constraint' rigid a -> a
    elem :: forall a. Eq a => a -> Constraint' rigid a -> Bool
    $celem :: forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
    length :: forall a. Constraint' rigid a -> Int
    $clength :: forall rigid a. Constraint' rigid a -> Int
    null :: forall a. Constraint' rigid a -> Bool
    $cnull :: forall rigid a. Constraint' rigid a -> Bool
    toList :: forall a. Constraint' rigid a -> [a]
    $ctoList :: forall rigid a. Constraint' rigid a -> [a]
    foldl1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
    $cfoldl1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
    foldr1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
    $cfoldr1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
    foldl' :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    $cfoldl' :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    foldl :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    $cfoldl :: forall rigid b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    foldr' :: forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    $cfoldr' :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    foldr :: forall a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    $cfoldr :: forall rigid a b. (a -> b -> b) -> b -> Constraint' rigid a -> b
    foldMap' :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    $cfoldMap' :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    foldMap :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    $cfoldMap :: forall rigid m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    fold :: forall m. Monoid m => Constraint' rigid m -> m
    $cfold :: forall rigid m. Monoid m => Constraint' rigid m -> m
    Foldable, Functor (Constraint' rigid)
    Foldable (Constraint' rigid)
    Functor (Constraint' rigid)
    -> Foldable (Constraint' rigid)
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b))
    -> (forall (f :: * -> *) a.
        Applicative f =>
        Constraint' rigid (f a) -> f (Constraint' rigid a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b))
    -> (forall (m :: * -> *) a.
        Monad m =>
        Constraint' rigid (m a) -> m (Constraint' rigid a))
    -> Traversable (Constraint' rigid)
    forall rigid. Functor (Constraint' rigid)
    forall rigid. Foldable (Constraint' rigid)
    forall rigid (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    forall rigid (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    forall (t :: * -> *).
    Functor t
    -> Foldable t
    -> (forall (f :: * -> *) a b.
        Applicative f =>
        (a -> f b) -> t a -> f (t b))
    -> (forall (f :: * -> *) a. Applicative f => t (f a) -> f (t a))
    -> (forall (m :: * -> *) a b.
        Monad m =>
        (a -> m b) -> t a -> m (t b))
    -> (forall (m :: * -> *) a. Monad m => t (m a) -> m (t a))
    -> Traversable t
    forall (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    forall (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    $csequence :: forall rigid (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    $cmapM :: forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    $csequenceA :: forall rigid (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    $ctraverse :: forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    Traversable)

    type Constraint = Constraint' Rigid Flex

    -- * Polarities to specify solutions.
    ------------------------------------------------------------------------

    -- | What type of solution are we looking for?
    data Polarity = Least | Greatest
      deriving (Polarity -> Polarity -> Bool
    (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Bool) -> Eq Polarity
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    /= :: Polarity -> Polarity -> Bool
    $c/= :: Polarity -> Polarity -> Bool
    == :: Polarity -> Polarity -> Bool
    $c== :: Polarity -> Polarity -> Bool
    Eq, Eq Polarity
    Eq Polarity
    -> (Polarity -> Polarity -> Ordering)
    -> (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Bool)
    -> (Polarity -> Polarity -> Polarity)
    -> (Polarity -> Polarity -> Polarity)
    -> Ord Polarity
    Polarity -> Polarity -> Bool
    Polarity -> Polarity -> Ordering
    Polarity -> Polarity -> Polarity
    forall a.
    Eq a
    -> (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    min :: Polarity -> Polarity -> Polarity
    $cmin :: Polarity -> Polarity -> Polarity
    max :: Polarity -> Polarity -> Polarity
    $cmax :: Polarity -> Polarity -> Polarity
    >= :: Polarity -> Polarity -> Bool
    $c>= :: Polarity -> Polarity -> Bool
    > :: Polarity -> Polarity -> Bool
    $c> :: Polarity -> Polarity -> Bool
    <= :: Polarity -> Polarity -> Bool
    $c<= :: Polarity -> Polarity -> Bool
    < :: Polarity -> Polarity -> Bool
    $c< :: Polarity -> Polarity -> Bool
    compare :: Polarity -> Polarity -> Ordering
    $ccompare :: Polarity -> Polarity -> Ordering
    Ord)

    -- | Assigning a polarity to a flexible variable.
    data PolarityAssignment flex = PolarityAssignment Polarity flex

    -- | Type of solution wanted for each flexible.
    type Polarities flex = Map flex Polarity

    emptyPolarities :: Polarities flex
    emptyPolarities :: forall flex. Polarities flex
    emptyPolarities = Map flex Polarity
    forall k a. Map k a
    Map.empty

    -- Used in size-solver (Andreas, 2021-08-20)
    polaritiesFromAssignments :: Ord flex => [PolarityAssignment flex] -> Polarities flex
    polaritiesFromAssignments :: forall flex.
    Ord flex =>
    [PolarityAssignment flex] -> Polarities flex
    polaritiesFromAssignments = (Polarity -> Polarity -> Polarity)
    -> [(flex, Polarity)] -> Map flex Polarity
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith Polarity -> Polarity -> Polarity
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(flex, Polarity)] -> Map flex Polarity)
    -> ([PolarityAssignment flex] -> [(flex, Polarity)])
    -> [PolarityAssignment flex]
    -> Map flex Polarity
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (PolarityAssignment flex -> (flex, Polarity))
    -> [PolarityAssignment flex] -> [(flex, Polarity)]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ (PolarityAssignment Polarity
    p flex
    x) -> (flex
    x,Polarity
    p))

    -- | Default polarity is 'Least'.
    getPolarity :: Ord flex => Polarities flex -> flex -> Polarity
    getPolarity :: forall flex. Ord flex => Polarities flex -> flex -> Polarity
    getPolarity Polarities flex
    pols flex
    x = Polarity -> flex -> Polarities flex -> Polarity
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Polarity
    Least flex
    x Polarities flex
    pols

    -- * Solutions.
    ------------------------------------------------------------------------

    -- | Partial substitution from flexible variables to size expression.
    newtype Solution rigid flex = Solution { forall rigid flex.
    Solution rigid flex -> Map flex (SizeExpr' rigid flex)
    theSolution :: Map flex (SizeExpr' rigid flex) }
      deriving (Int -> Solution rigid flex -> ShowS
    [Solution rigid flex] -> ShowS
    Solution rigid flex -> String
    (Int -> Solution rigid flex -> ShowS)
    -> (Solution rigid flex -> String)
    -> ([Solution rigid flex] -> ShowS)
    -> Show (Solution rigid flex)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall rigid flex.
    (Show flex, Show rigid) =>
    Int -> Solution rigid flex -> ShowS
    forall rigid flex.
    (Show flex, Show rigid) =>
    [Solution rigid flex] -> ShowS
    forall rigid flex.
    (Show flex, Show rigid) =>
    Solution rigid flex -> String
    showList :: [Solution rigid flex] -> ShowS
    $cshowList :: forall rigid flex.
    (Show flex, Show rigid) =>
    [Solution rigid flex] -> ShowS
    show :: Solution rigid flex -> String
    $cshow :: forall rigid flex.
    (Show flex, Show rigid) =>
    Solution rigid flex -> String
    showsPrec :: Int -> Solution rigid flex -> ShowS
    $cshowsPrec :: forall rigid flex.
    (Show flex, Show rigid) =>
    Int -> Solution rigid flex -> ShowS
    Show, Solution rigid flex
    Solution rigid flex -> Bool
    Solution rigid flex
    -> (Solution rigid flex -> Bool) -> Null (Solution rigid flex)
    forall a. a -> (a -> Bool) -> Null a
    forall rigid flex. Solution rigid flex
    forall rigid flex. Solution rigid flex -> Bool
    null :: Solution rigid flex -> Bool
    $cnull :: forall rigid flex. Solution rigid flex -> Bool
    empty :: Solution rigid flex
    $cempty :: forall rigid flex. Solution rigid flex
    Null)

    instance (Pretty r, Pretty f) => Pretty (Solution r f) where
      pretty :: Solution r f -> Doc
    pretty (Solution Map f (SizeExpr' r f)
    sol) = [Doc] -> Doc
    forall a. Pretty a => [a] -> Doc
    prettyList ([Doc] -> Doc) -> [Doc] -> Doc
    forall a b. (a -> b) -> a -> b
    $ [(f, SizeExpr' r f)] -> ((f, SizeExpr' r f) -> Doc) -> [Doc]
    forall (m :: * -> *) a b. Functor m => m a -> (a -> b) -> m b
    for (Map f (SizeExpr' r f) -> [(f, SizeExpr' r f)]
    forall k a. Map k a -> [(k, a)]
    Map.toList Map f (SizeExpr' r f)
    sol) (((f, SizeExpr' r f) -> Doc) -> [Doc])
    -> ((f, SizeExpr' r f) -> Doc) -> [Doc]
    forall a b. (a -> b) -> a -> b
    $ \ (f
    x, SizeExpr' r f
    e) ->
        f -> Doc
    forall a. Pretty a => a -> Doc
    pretty f
    x Doc -> Doc -> Doc
    <+> Doc
    ":=" Doc -> Doc -> Doc
    <+> SizeExpr' r f -> Doc
    forall a. Pretty a => a -> Doc
    pretty SizeExpr' r f
    e

    emptySolution :: Solution r f
    emptySolution :: forall rigid flex. Solution rigid flex
    emptySolution = Map f (SizeExpr' r f) -> Solution r f
    forall rigid flex.
    Map flex (SizeExpr' rigid flex) -> Solution rigid flex
    Solution Map f (SizeExpr' r f)
    forall k a. Map k a
    Map.empty

    -- | Executing a substitution.
    class Substitute r f a where
      subst :: Solution r f -> a -> a

    instance Ord f => Substitute r f (SizeExpr' r f) where
      subst :: Solution r f -> SizeExpr' r f -> SizeExpr' r f
    subst (Solution Map f (SizeExpr' r f)
    sol) SizeExpr' r f
    e =
        case SizeExpr' r f
    e of
          Flex f
    x Offset
    n -> SizeExpr' r f
    -> (SizeExpr' r f -> SizeExpr' r f)
    -> Maybe (SizeExpr' r f)
    -> SizeExpr' r f
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe SizeExpr' r f
    e (SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Offset
    n) (Maybe (SizeExpr' r f) -> SizeExpr' r f)
    -> Maybe (SizeExpr' r f) -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ f -> Map f (SizeExpr' r f) -> Maybe (SizeExpr' r f)
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup f
    x Map f (SizeExpr' r f)
    sol
          SizeExpr' r f
    _        -> SizeExpr' r f
    e

    instance Ord f => Substitute r f (Constraint' r f) where
      subst :: Solution r f -> Constraint' r f -> Constraint' r f
    subst Solution r f
    sol (Constraint SizeExpr' r f
    e Cmp
    cmp SizeExpr' r f
    e') = SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (Solution r f -> SizeExpr' r f -> SizeExpr' r f
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst Solution r f
    sol SizeExpr' r f
    e) Cmp
    cmp (Solution r f -> SizeExpr' r f -> SizeExpr' r f
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst Solution r f
    sol SizeExpr' r f
    e')

    instance Substitute r f a => Substitute r f [a] where
      subst :: Solution r f -> [a] -> [a]
    subst = (a -> a) -> [a] -> [a]
    forall a b. (a -> b) -> [a] -> [b]
    map ((a -> a) -> [a] -> [a])
    -> (Solution r f -> a -> a) -> Solution r f -> [a] -> [a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Solution r f -> a -> a
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst

    instance Substitute r f a => Substitute r f (Map k a) where
      subst :: Solution r f -> Map k a -> Map k a
    subst = (a -> a) -> Map k a -> Map k a
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap ((a -> a) -> Map k a -> Map k a)
    -> (Solution r f -> a -> a) -> Solution r f -> Map k a -> Map k a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Solution r f -> a -> a
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst

    instance Ord f => Substitute r f (Solution r f) where
      subst :: Solution r f -> Solution r f -> Solution r f
    subst Solution r f
    s = Map f (SizeExpr' r f) -> Solution r f
    forall rigid flex.
    Map flex (SizeExpr' rigid flex) -> Solution rigid flex
    Solution (Map f (SizeExpr' r f) -> Solution r f)
    -> (Solution r f -> Map f (SizeExpr' r f))
    -> Solution r f
    -> Solution r f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Solution r f -> Map f (SizeExpr' r f) -> Map f (SizeExpr' r f)
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst Solution r f
    s (Map f (SizeExpr' r f) -> Map f (SizeExpr' r f))
    -> (Solution r f -> Map f (SizeExpr' r f))
    -> Solution r f
    -> Map f (SizeExpr' r f)
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Solution r f -> Map f (SizeExpr' r f)
    forall rigid flex.
    Solution rigid flex -> Map flex (SizeExpr' rigid flex)
    theSolution

    -- | Add offset to size expression.
    instance Plus (SizeExpr' r f) Offset (SizeExpr' r f) where
      plus :: SizeExpr' r f -> Offset -> SizeExpr' r f
    plus SizeExpr' r f
    e Offset
    m =
        case SizeExpr' r f
    e of
          Const   Offset
    n -> Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const   (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    m
          Rigid r
    i Offset
    n -> r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    m
          Flex f
    x  Offset
    n -> f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x  (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    m
          SizeExpr' r f
    Infty     -> SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty

    -- * Constraint simplification

    type CTrans r f = Constraint' r f -> Either String [Constraint' r f]

    -- | Returns an error message if we have a contradictory constraint.
    simplify1 :: (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    simplify1 :: forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    simplify1 CTrans r f
    test Constraint' r f
    c = do
      let err :: Either String [Constraint' r f]
    err = String -> Either String [Constraint' r f]
    forall a b. a -> Either a b
    Left (String -> Either String [Constraint' r f])
    -> String -> Either String [Constraint' r f]
    forall a b. (a -> b) -> a -> b
    $ String
    "size constraint " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Constraint' r f -> String
    forall a. Pretty a => a -> String
    prettyShow Constraint' r f
    c String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " is inconsistent"
      case Constraint' r f
    c of
        -- rhs is Infty
        Constraint SizeExpr' r f
    a           Cmp
    Le  SizeExpr' r f
    Infty -> [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Constraint Const{}     Cmp
    Lt  SizeExpr' r f
    Infty -> [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Constraint SizeExpr' r f
    Infty       Cmp
    Lt  SizeExpr' r f
    Infty -> Either String [Constraint' r f]
    err
        Constraint (Rigid r
    i Offset
    n) Cmp
    Lt  SizeExpr' r f
    Infty -> CTrans r f
    test CTrans r f -> CTrans r f
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i Offset
    0) Cmp
    Lt SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty
        Constraint a :: SizeExpr' r f
    a@Flex{}    Cmp
    Lt  SizeExpr' r f
    Infty -> [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint' r f
    c { leftExpr :: SizeExpr' r f
    leftExpr = SizeExpr' r f
    a { offset :: Offset
    offset = Offset
    0 }}]

        -- rhs is Const
        Constraint (Const Offset
    n)   Cmp
    cmp (Const Offset
    m) -> if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    n Cmp
    cmp Offset
    m then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else Either String [Constraint' r f]
    err
        Constraint SizeExpr' r f
    Infty       Cmp
    cmp  Const{}  -> Either String [Constraint' r f]
    err
        Constraint (Rigid r
    i Offset
    n) Cmp
    cmp (Const Offset
    m) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    n Cmp
    cmp Offset
    m then
            CTrans r f
    test (SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i Offset
    0) Cmp
    Le (Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const (Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Cmp -> Offset -> Offset -> Offset
    forall a. Cmp -> a -> a -> a
    ifLe Cmp
    cmp Offset
    0 Offset
    1)))
           else Either String [Constraint' r f]
    err
        Constraint (Flex f
    x Offset
    n)  Cmp
    cmp (Const Offset
    m) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    n Cmp
    cmp Offset
    m
           then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0) Cmp
    Le (Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const (Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Cmp -> Offset -> Offset -> Offset
    forall a. Cmp -> a -> a -> a
    ifLe Cmp
    cmp Offset
    0 Offset
    1))]
           else Either String [Constraint' r f]
    err

        -- rhs is Rigid
        Constraint SizeExpr' r f
    Infty Cmp
    cmp Rigid{} -> Either String [Constraint' r f]
    err
        Constraint (Const Offset
    m) Cmp
    cmp (Rigid r
    i Offset
    n) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          else CTrans r f
    test (SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n) Cmp
    cmp (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i Offset
    0))
        Constraint (Rigid r
    j Offset
    m) Cmp
    cmp (Rigid r
    i Offset
    n) | r
    i r -> r -> Bool
    forall a. Eq a => a -> a -> Bool
    == r
    j ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else Either String [Constraint' r f]
    err
        Constraint (Rigid r
    j Offset
    m) Cmp
    cmp (Rigid r
    i Offset
    n) -> CTrans r f
    test Constraint' r f
    c
        Constraint (Flex f
    x Offset
    m)  Cmp
    cmp (Rigid r
    i Offset
    n) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n
           then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0) Cmp
    Le (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i (Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Cmp -> Offset -> Offset -> Offset
    forall a. Cmp -> a -> a -> a
    ifLe Cmp
    cmp Offset
    0 Offset
    1))]
           else [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Cmp -> Offset -> Offset -> Offset
    forall a. Cmp -> a -> a -> a
    ifLe Cmp
    cmp Offset
    0 Offset
    1) Cmp
    Le (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i Offset
    0)]

        -- rhs is Flex
        Constraint SizeExpr' r f
    Infty Cmp
    Le (Flex f
    x Offset
    n) -> [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty Cmp
    Le (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0)]
        Constraint SizeExpr' r f
    Infty Cmp
    Lt (Flex f
    x Offset
    n) -> Either String [Constraint' r f]
    err
        Constraint (Const Offset
    m) Cmp
    cmp (Flex f
    x Offset
    n) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          else [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Cmp -> Offset -> Offset -> Offset
    forall a. Cmp -> a -> a -> a
    ifLe Cmp
    cmp Offset
    0 Offset
    1) Cmp
    Le (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0)]
        Constraint (Rigid r
    i Offset
    m) Cmp
    cmp (Flex f
    x Offset
    n) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n
          then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i Offset
    0) Cmp
    cmp (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    m)]
          else [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n) Cmp
    cmp (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0)]
        Constraint (Flex f
    y Offset
    m) Cmp
    cmp (Flex f
    x Offset
    n) ->
          if Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    m Cmp
    cmp Offset
    n
          then [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    y Offset
    0) Cmp
    cmp (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    n Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    m)]
          else [Constraint' r f] -> Either String [Constraint' r f]
    forall (m :: * -> *) a. Monad m => a -> m a
    return [SizeExpr' r f -> Cmp -> SizeExpr' r f -> Constraint' r f
    forall rigid flex.
    SizeExpr' rigid flex
    -> Cmp -> SizeExpr' rigid flex -> Constraint' rigid flex
    Constraint (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    y (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n) Cmp
    cmp (f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex f
    x Offset
    0)]

    -- | 'Le' acts as 'True', 'Lt' as 'False'.
    ifLe :: Cmp -> a -> a -> a
    ifLe :: forall a. Cmp -> a -> a -> a
    ifLe Cmp
    Le a
    a a
    b = a
    a
    ifLe Cmp
    Lt a
    a a
    b = a
    b

    -- | Interpret 'Cmp' as relation on 'Offset'.
    compareOffset :: Offset -> Cmp -> Offset -> Bool
    compareOffset :: Offset -> Cmp -> Offset -> Bool
    compareOffset Offset
    n Cmp
    Le Offset
    m = Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    m
    compareOffset Offset
    n Cmp
    Lt Offset
    m = Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <  Offset
    m

    -- * Printing

    instance (Pretty r, Pretty f) => Pretty (SizeExpr' r f) where
      pretty :: SizeExpr' r f -> Doc
    pretty (Const Offset
    n)   = Offset -> Doc
    forall a. Pretty a => a -> Doc
    pretty Offset
    n
      pretty (SizeExpr' r f
    Infty)     = Doc
    "∞"
      pretty (Rigid r
    i Offset
    0) = r -> Doc
    forall a. Pretty a => a -> Doc
    pretty r
    i
      pretty (Rigid r
    i Offset
    n) = r -> Doc
    forall a. Pretty a => a -> Doc
    pretty r
    i Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc
    text (String
    "+" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Offset -> String
    forall a. Show a => a -> String
    show Offset
    n)
      pretty (Flex  f
    x Offset
    0) = f -> Doc
    forall a. Pretty a => a -> Doc
    pretty f
    x
      pretty (Flex  f
    x Offset
    n) = f -> Doc
    forall a. Pretty a => a -> Doc
    pretty f
    x Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc
    text (String
    "+" String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Offset -> String
    forall a. Show a => a -> String
    show Offset
    n)

    instance Pretty Polarity where
      pretty :: Polarity -> Doc
    pretty Polarity
    Least    = Doc
    "-"
      pretty Polarity
    Greatest = Doc
    "+"

    instance Pretty flex => Pretty (PolarityAssignment flex) where
      pretty :: PolarityAssignment flex -> Doc
    pretty (PolarityAssignment Polarity
    pol flex
    flex) = Polarity -> Doc
    forall a. Pretty a => a -> Doc
    pretty Polarity
    pol Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> flex -> Doc
    forall a. Pretty a => a -> Doc
    pretty flex
    flex

    instance Pretty Cmp where
      pretty :: Cmp -> Doc
    pretty Cmp
    Le = Doc
    "≤"
      pretty Cmp
    Lt = Doc
    "<"

    instance (Pretty r, Pretty f) => Pretty (Constraint' r f) where
      pretty :: Constraint' r f -> Doc
    pretty (Constraint SizeExpr' r f
    a Cmp
    cmp SizeExpr' r f
    b) = SizeExpr' r f -> Doc
    forall a. Pretty a => a -> Doc
    pretty SizeExpr' r f
    a Doc -> Doc -> Doc
    <+> Cmp -> Doc
    forall a. Pretty a => a -> Doc
    pretty Cmp
    cmp Doc -> Doc -> Doc
    <+> SizeExpr' r f -> Doc
    forall a. Pretty a => a -> Doc
    pretty SizeExpr' r f
    b

    -- * Wellformedness

    -- | Offsets @+ n@ must be non-negative
    class ValidOffset a where
      validOffset :: a -> Bool

    instance ValidOffset Offset where
      validOffset :: Offset -> Bool
    validOffset = (Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    0)

    instance ValidOffset (SizeExpr' r f) where
      validOffset :: SizeExpr' r f -> Bool
    validOffset SizeExpr' r f
    e =
        case SizeExpr' r f
    e of
          SizeExpr' r f
    Infty -> Bool
    True
          SizeExpr' r f
    _     -> Offset -> Bool
    forall a. ValidOffset a => a -> Bool
    validOffset (SizeExpr' r f -> Offset
    forall rigid flex. SizeExpr' rigid flex -> Offset
    offset SizeExpr' r f
    e)

    -- | Make offsets non-negative by rounding up.
    class TruncateOffset a where
      truncateOffset :: a -> a

    instance TruncateOffset Offset where
      truncateOffset :: Offset -> Offset
    truncateOffset Offset
    n | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    0    = Offset
    n
                       | Bool
    otherwise = Offset
    0

    instance TruncateOffset (SizeExpr' r f) where
      truncateOffset :: SizeExpr' r f -> SizeExpr' r f
    truncateOffset SizeExpr' r f
    e =
        case SizeExpr' r f
    e of
          SizeExpr' r f
    Infty     -> SizeExpr' r f
    e
          Const Offset
    n   -> Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const   (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. TruncateOffset a => a -> a
    truncateOffset Offset
    n
          Rigid r
    i Offset
    n -> r -> Offset -> SizeExpr' r f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid r
    i (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. TruncateOffset a => a -> a
    truncateOffset Offset
    n
          Flex  f
    x Offset
    n -> f -> Offset -> SizeExpr' r f
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex  f
    x (Offset -> SizeExpr' r f) -> Offset -> SizeExpr' r f
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. TruncateOffset a => a -> a
    truncateOffset Offset
    n

    -- * Computing variable sets

    -- | The rigid variables contained in a pice of syntax.
    class Ord (RigidOf a) => Rigids a where
      type RigidOf a
      rigids :: a -> Set (RigidOf a)

    instance Rigids a => Rigids [a] where
      type RigidOf [a] = RigidOf a
      rigids :: [a] -> Set (RigidOf [a])
    rigids [a]
    as = [Set (RigidOf a)] -> Set (RigidOf a)
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ((a -> Set (RigidOf a)) -> [a] -> [Set (RigidOf a)]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Set (RigidOf a)
    forall a. Rigids a => a -> Set (RigidOf a)
    rigids [a]
    as)

    instance Ord r => Rigids (SizeExpr' r f) where
      type RigidOf (SizeExpr' r f) = r
      rigids :: SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
    rigids (Rigid r
    x Offset
    _) = r -> Set r
    forall a. a -> Set a
    Set.singleton r
    x

      rigids SizeExpr' r f
    _           = Set (RigidOf (SizeExpr' r f))
    forall a. Set a
    Set.empty

    instance Ord r => Rigids (Constraint' r f) where
      type RigidOf (Constraint' r f) = r
      rigids :: Constraint' r f -> Set (RigidOf (Constraint' r f))
    rigids (Constraint SizeExpr' r f
    l Cmp
    _ SizeExpr' r f
    r) = Set r -> Set r -> Set r
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
    forall a. Rigids a => a -> Set (RigidOf a)
    rigids SizeExpr' r f
    l) (SizeExpr' r f -> Set (RigidOf (SizeExpr' r f))
    forall a. Rigids a => a -> Set (RigidOf a)
    rigids SizeExpr' r f
    r)

    -- | The flexibe variables contained in a pice of syntax.
    class Ord (FlexOf a) => Flexs a where
      type FlexOf a
      flexs :: a -> Set (FlexOf a)

    instance Flexs a => Flexs [a] where
      type FlexOf [a] = FlexOf a
      flexs :: [a] -> Set (FlexOf [a])
    flexs [a]
    as = [Set (FlexOf a)] -> Set (FlexOf a)
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions ((a -> Set (FlexOf a)) -> [a] -> [Set (FlexOf a)]
    forall a b. (a -> b) -> [a] -> [b]
    map a -> Set (FlexOf a)
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs [a]
    as)

    instance Ord flex => Flexs (SizeExpr' rigid flex) where
      type FlexOf (SizeExpr' rigid flex) = flex
      flexs :: SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
    flexs (Flex flex
    x Offset
    _) = flex -> Set flex
    forall a. a -> Set a
    Set.singleton flex
    x
      flexs SizeExpr' rigid flex
    _          = Set (FlexOf (SizeExpr' rigid flex))
    forall a. Set a
    Set.empty

    instance Ord flex => Flexs (Constraint' rigid flex) where
      type FlexOf (Constraint' rigid flex) = flex
      flexs :: Constraint' rigid flex -> Set (FlexOf (Constraint' rigid flex))
    flexs (Constraint SizeExpr' rigid flex
    l Cmp
    _ SizeExpr' rigid flex
    r) = Set flex -> Set flex -> Set flex
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union (SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs SizeExpr' rigid flex
    l) (SizeExpr' rigid flex -> Set (FlexOf (SizeExpr' rigid flex))
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs SizeExpr' rigid flex
    r)