    {-# OPTIONS_GHC -Wunused-imports #-}

    -- | Syntax of size expressions and constraints.

    module Agda.TypeChecking.SizedTypes.Syntax where

    import Prelude hiding ( null )

    import GHC.Generics (Generic)
    import Control.DeepSeq

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

    import Agda.Syntax.Common

    import Agda.TypeChecking.Monad.Base.Types hiding (Polarity)
    import Agda.TypeChecking.SizedTypes.Utils

    import Agda.Utils.Function
    import Agda.Utils.Functor
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty as P

    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
    $c== :: Offset -> Offset -> Bool
    == :: Offset -> Offset -> Bool
    $c/= :: Offset -> Offset -> Bool
    /= :: 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
    $ccompare :: Offset -> Offset -> Ordering
    compare :: Offset -> Offset -> Ordering
    $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
    >= :: Offset -> Offset -> Bool
    $cmax :: Offset -> Offset -> Offset
    max :: Offset -> Offset -> Offset
    $cmin :: Offset -> Offset -> Offset
    min :: Offset -> Offset -> Offset
    Ord, (forall x. Offset -> Rep Offset x)
    -> (forall x. Rep Offset x -> Offset) -> Generic Offset
    forall x. Rep Offset x -> Offset
    forall x. Offset -> Rep Offset x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Offset -> Rep Offset x
    from :: forall x. Offset -> Rep Offset x
    $cto :: forall x. Rep Offset x -> Offset
    to :: forall x. Rep Offset x -> Offset
    Generic, 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
    $c+ :: Offset -> Offset -> Offset
    + :: Offset -> Offset -> Offset
    $c- :: Offset -> Offset -> Offset
    - :: Offset -> Offset -> Offset
    $c* :: Offset -> Offset -> Offset
    * :: Offset -> Offset -> Offset
    $cnegate :: Offset -> Offset
    negate :: Offset -> Offset
    $cabs :: Offset -> Offset
    abs :: Offset -> Offset
    $csignum :: Offset -> Offset
    signum :: Offset -> Offset
    $cfromInteger :: Integer -> Offset
    fromInteger :: Integer -> 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
    $csucc :: Offset -> Offset
    succ :: Offset -> Offset
    $cpred :: Offset -> Offset
    pred :: Offset -> Offset
    $ctoEnum :: Int -> Offset
    toEnum :: Int -> Offset
    $cfromEnum :: Offset -> Int
    fromEnum :: Offset -> Int
    $cenumFrom :: Offset -> [Offset]
    enumFrom :: Offset -> [Offset]
    $cenumFromThen :: Offset -> Offset -> [Offset]
    enumFromThen :: Offset -> Offset -> [Offset]
    $cenumFromTo :: Offset -> Offset -> [Offset]
    enumFromTo :: Offset -> Offset -> [Offset]
    $cenumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
    enumFromThenTo :: Offset -> Offset -> Offset -> [Offset]
    Enum)

    instance NFData Offset

    -- 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
    $c== :: Rigid -> Rigid -> Bool
    == :: Rigid -> Rigid -> Bool
    $c/= :: Rigid -> Rigid -> Bool
    /= :: 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
    $ccompare :: Rigid -> Rigid -> Ordering
    compare :: Rigid -> Rigid -> Ordering
    $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
    >= :: Rigid -> Rigid -> Bool
    $cmax :: Rigid -> Rigid -> Rigid
    max :: Rigid -> Rigid -> Rigid
    $cmin :: Rigid -> Rigid -> Rigid
    min :: Rigid -> Rigid -> Rigid
    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
    forall a. String -> Doc a
    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
    $c== :: Flex -> Flex -> Bool
    == :: Flex -> Flex -> Bool
    $c/= :: Flex -> Flex -> Bool
    /= :: 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
    $ccompare :: Flex -> Flex -> Ordering
    compare :: Flex -> Flex -> Ordering
    $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
    >= :: Flex -> Flex -> Bool
    $cmax :: Flex -> Flex -> Flex
    max :: Flex -> Flex -> Flex
    $cmin :: Flex -> Flex -> Flex
    min :: Flex -> Flex -> Flex
    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
    forall a. String -> Doc a
    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
    $cshowsPrec :: forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> SizeExpr' rigid flex -> ShowS
    showsPrec :: Int -> SizeExpr' rigid flex -> ShowS
    $cshow :: forall rigid flex.
    (Show rigid, Show flex) =>
    SizeExpr' rigid flex -> String
    show :: SizeExpr' rigid flex -> String
    $cshowList :: forall rigid flex.
    (Show rigid, Show flex) =>
    [SizeExpr' rigid flex] -> ShowS
    showList :: [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
    $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
    /= :: 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
    $ccompare :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    compare :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Ordering
    $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
    >= :: SizeExpr' rigid flex -> SizeExpr' rigid flex -> Bool
    $cmax :: 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
    $cmin :: 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
    Ord, (forall x. SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x)
    -> (forall x. Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex)
    -> Generic (SizeExpr' rigid flex)
    forall x. Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex
    forall x. SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall rigid flex x.
    Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex
    forall rigid flex x.
    SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x
    $cfrom :: forall rigid flex x.
    SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x
    from :: forall x. SizeExpr' rigid flex -> Rep (SizeExpr' rigid flex) x
    $cto :: forall rigid flex x.
    Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex
    to :: forall x. Rep (SizeExpr' rigid flex) x -> SizeExpr' rigid flex
    Generic, (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
    $cfmap :: forall rigid a b.
    (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    fmap :: forall a b. (a -> b) -> SizeExpr' rigid a -> SizeExpr' rigid b
    $c<$ :: forall rigid a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    <$ :: forall a b. a -> SizeExpr' rigid b -> SizeExpr' rigid a
    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
    $cfold :: forall rigid m. Monoid m => SizeExpr' rigid m -> m
    fold :: forall m. Monoid m => SizeExpr' rigid m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> SizeExpr' rigid a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> SizeExpr' rigid a -> b
    $cfoldr1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
    foldr1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
    $cfoldl1 :: forall rigid a. (a -> a -> a) -> SizeExpr' rigid a -> a
    foldl1 :: forall a. (a -> a -> a) -> SizeExpr' rigid a -> a
    $ctoList :: forall rigid a. SizeExpr' rigid a -> [a]
    toList :: forall a. SizeExpr' rigid a -> [a]
    $cnull :: forall rigid a. SizeExpr' rigid a -> Bool
    null :: forall a. SizeExpr' rigid a -> Bool
    $clength :: forall rigid a. SizeExpr' rigid a -> Int
    length :: forall a. SizeExpr' rigid a -> Int
    $celem :: forall rigid a. Eq a => a -> SizeExpr' rigid a -> Bool
    elem :: forall a. Eq a => a -> SizeExpr' rigid a -> Bool
    $cmaximum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
    maximum :: forall a. Ord a => SizeExpr' rigid a -> a
    $cminimum :: forall rigid a. Ord a => SizeExpr' rigid a -> a
    minimum :: forall a. Ord a => SizeExpr' rigid a -> a
    $csum :: forall rigid a. Num a => SizeExpr' rigid a -> a
    sum :: forall a. Num a => SizeExpr' rigid a -> a
    $cproduct :: forall rigid a. Num a => SizeExpr' rigid a -> a
    product :: forall a. Num a => SizeExpr' rigid a -> a
    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)
    $ctraverse :: forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> SizeExpr' rigid a -> f (SizeExpr' rigid b)
    $csequenceA :: forall rigid (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    SizeExpr' rigid (f a) -> f (SizeExpr' rigid a)
    $cmapM :: forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> SizeExpr' rigid a -> m (SizeExpr' rigid b)
    $csequence :: forall rigid (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    SizeExpr' rigid (m a) -> m (SizeExpr' rigid a)
    Traversable)

    type SizeExpr = SizeExpr' Rigid Flex

    instance (NFData r, NFData f) => NFData (SizeExpr' r f)

    -- | 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
    $cshowsPrec :: Int -> Cmp -> ShowS
    showsPrec :: Int -> Cmp -> ShowS
    $cshow :: Cmp -> String
    show :: Cmp -> String
    $cshowList :: [Cmp] -> ShowS
    showList :: [Cmp] -> ShowS
    Show, Cmp -> Cmp -> Bool
    (Cmp -> Cmp -> Bool) -> (Cmp -> Cmp -> Bool) -> Eq Cmp
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Cmp -> Cmp -> Bool
    == :: Cmp -> Cmp -> Bool
    $c/= :: Cmp -> Cmp -> Bool
    /= :: Cmp -> Cmp -> Bool
    Eq, (forall x. Cmp -> Rep Cmp x)
    -> (forall x. Rep Cmp x -> Cmp) -> Generic Cmp
    forall x. Rep Cmp x -> Cmp
    forall x. Cmp -> Rep Cmp x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. Cmp -> Rep Cmp x
    from :: forall x. Cmp -> Rep Cmp x
    $cto :: forall x. Rep Cmp x -> Cmp
    to :: forall x. Rep Cmp x -> Cmp
    Generic, Cmp
    Cmp -> Cmp -> Bounded Cmp
    forall a. a -> a -> Bounded a
    $cminBound :: Cmp
    minBound :: Cmp
    $cmaxBound :: Cmp
    maxBound :: 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
    $csucc :: Cmp -> Cmp
    succ :: Cmp -> Cmp
    $cpred :: Cmp -> Cmp
    pred :: Cmp -> Cmp
    $ctoEnum :: Int -> Cmp
    toEnum :: Int -> Cmp
    $cfromEnum :: Cmp -> Int
    fromEnum :: Cmp -> Int
    $cenumFrom :: Cmp -> [Cmp]
    enumFrom :: Cmp -> [Cmp]
    $cenumFromThen :: Cmp -> Cmp -> [Cmp]
    enumFromThen :: Cmp -> Cmp -> [Cmp]
    $cenumFromTo :: Cmp -> Cmp -> [Cmp]
    enumFromTo :: Cmp -> Cmp -> [Cmp]
    $cenumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
    enumFromThenTo :: Cmp -> Cmp -> Cmp -> [Cmp]
    Enum)

    instance NFData Cmp

    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
    $cshowsPrec :: forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> Constraint' rigid flex -> ShowS
    showsPrec :: Int -> Constraint' rigid flex -> ShowS
    $cshow :: forall rigid flex.
    (Show rigid, Show flex) =>
    Constraint' rigid flex -> String
    show :: Constraint' rigid flex -> String
    $cshowList :: forall rigid flex.
    (Show rigid, Show flex) =>
    [Constraint' rigid flex] -> ShowS
    showList :: [Constraint' rigid flex] -> ShowS
    Show, (forall x.
     Constraint' rigid flex -> Rep (Constraint' rigid flex) x)
    -> (forall x.
        Rep (Constraint' rigid flex) x -> Constraint' rigid flex)
    -> Generic (Constraint' rigid flex)
    forall x. Rep (Constraint' rigid flex) x -> Constraint' rigid flex
    forall x. Constraint' rigid flex -> Rep (Constraint' rigid flex) x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    forall rigid flex x.
    Rep (Constraint' rigid flex) x -> Constraint' rigid flex
    forall rigid flex x.
    Constraint' rigid flex -> Rep (Constraint' rigid flex) x
    $cfrom :: forall rigid flex x.
    Constraint' rigid flex -> Rep (Constraint' rigid flex) x
    from :: forall x. Constraint' rigid flex -> Rep (Constraint' rigid flex) x
    $cto :: forall rigid flex x.
    Rep (Constraint' rigid flex) x -> Constraint' rigid flex
    to :: forall x. Rep (Constraint' rigid flex) x -> Constraint' rigid flex
    Generic, (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
    $cfmap :: forall rigid a b.
    (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    fmap :: forall a b. (a -> b) -> Constraint' rigid a -> Constraint' rigid b
    $c<$ :: forall rigid a b. a -> Constraint' rigid b -> Constraint' rigid a
    <$ :: forall a b. a -> Constraint' rigid b -> Constraint' rigid a
    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
    $cfold :: forall rigid m. Monoid m => Constraint' rigid m -> m
    fold :: forall m. Monoid m => Constraint' rigid m -> 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
    foldMap' :: forall m a. Monoid m => (a -> m) -> Constraint' rigid a -> m
    $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
    foldr' :: forall a b. (a -> b -> 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
    foldl' :: forall b a. (b -> a -> b) -> b -> Constraint' rigid a -> b
    $cfoldr1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
    foldr1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
    $cfoldl1 :: forall rigid a. (a -> a -> a) -> Constraint' rigid a -> a
    foldl1 :: forall a. (a -> a -> a) -> Constraint' rigid a -> a
    $ctoList :: forall rigid a. Constraint' rigid a -> [a]
    toList :: forall a. Constraint' rigid a -> [a]
    $cnull :: forall rigid a. Constraint' rigid a -> Bool
    null :: forall a. Constraint' rigid a -> Bool
    $clength :: forall rigid a. Constraint' rigid a -> Int
    length :: forall a. Constraint' rigid a -> Int
    $celem :: forall rigid a. Eq a => a -> Constraint' rigid a -> Bool
    elem :: forall a. Eq a => a -> Constraint' rigid a -> Bool
    $cmaximum :: forall rigid a. Ord a => Constraint' rigid a -> a
    maximum :: forall a. Ord a => Constraint' rigid a -> a
    $cminimum :: forall rigid a. Ord a => Constraint' rigid a -> a
    minimum :: forall a. Ord a => Constraint' rigid a -> a
    $csum :: forall rigid a. Num a => Constraint' rigid a -> a
    sum :: forall a. Num a => Constraint' rigid a -> a
    $cproduct :: forall rigid a. Num a => Constraint' rigid a -> a
    product :: forall a. Num a => Constraint' rigid a -> a
    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)
    $ctraverse :: forall rigid (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    traverse :: forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Constraint' rigid a -> f (Constraint' rigid b)
    $csequenceA :: forall rigid (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    sequenceA :: forall (f :: * -> *) a.
    Applicative f =>
    Constraint' rigid (f a) -> f (Constraint' rigid a)
    $cmapM :: forall rigid (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    mapM :: forall (m :: * -> *) a b.
    Monad m =>
    (a -> m b) -> Constraint' rigid a -> m (Constraint' rigid b)
    $csequence :: forall rigid (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    sequence :: forall (m :: * -> *) a.
    Monad m =>
    Constraint' rigid (m a) -> m (Constraint' rigid a)
    Traversable)

    type Constraint = Constraint' Rigid Flex

    instance (NFData r, NFData f) => NFData (Constraint' r f)

    -- * 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
    $c== :: Polarity -> Polarity -> Bool
    == :: Polarity -> Polarity -> Bool
    $c/= :: Polarity -> Polarity -> Bool
    /= :: 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
    $ccompare :: Polarity -> Polarity -> Ordering
    compare :: Polarity -> Polarity -> Ordering
    $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
    >= :: Polarity -> Polarity -> Bool
    $cmax :: Polarity -> Polarity -> Polarity
    max :: Polarity -> Polarity -> Polarity
    $cmin :: Polarity -> Polarity -> Polarity
    min :: Polarity -> Polarity -> Polarity
    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
    $cshowsPrec :: forall rigid flex.
    (Show flex, Show rigid) =>
    Int -> Solution rigid flex -> ShowS
    showsPrec :: Int -> Solution rigid flex -> ShowS
    $cshow :: forall rigid flex.
    (Show flex, Show rigid) =>
    Solution rigid flex -> String
    show :: Solution rigid flex -> String
    $cshowList :: forall rigid flex.
    (Show flex, Show rigid) =>
    [Solution rigid flex] -> ShowS
    showList :: [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
    $cempty :: forall rigid flex. Solution rigid flex
    empty :: Solution rigid flex
    $cnull :: forall rigid flex. Solution rigid flex -> Bool
    null :: Solution rigid flex -> Bool
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc
    ":=" Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> 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 a b. (a -> b) -> Map k a -> Map k b
    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 -> Maybe [Constraint' r f]

    -- | Returns 'Nothing' if the constraint is contradictory.
    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 :: Maybe a
    err = Maybe a
    forall a. Maybe a
    Nothing
      case Constraint' r f
    c of
        -- rhs is Infty
        Constraint SizeExpr' r f
    a           Cmp
    Le  SizeExpr' r f
    Infty -> [Constraint' r f] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Constraint Const{}     Cmp
    Lt  SizeExpr' r f
    Infty -> [Constraint' r f] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
        Constraint SizeExpr' r f
    Infty       Cmp
    Lt  SizeExpr' r f
    Infty -> Maybe [Constraint' r f]
    forall a. Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint' r f
    c { leftExpr = a { 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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else Maybe [Constraint' r f]
    forall a. Maybe a
    err
        Constraint SizeExpr' r f
    Infty       Cmp
    cmp  Const{}  -> Maybe [Constraint' r f]
    forall a. Maybe a
    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 Maybe [Constraint' r f]
    forall a. Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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 Maybe [Constraint' r f]
    forall a. Maybe a
    err

        -- rhs is Rigid
        Constraint SizeExpr' r f
    Infty Cmp
    cmp Rigid{} -> Maybe [Constraint' r f]
    forall a. Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [] else Maybe [Constraint' r f]
    forall a. Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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) -> Maybe [Constraint' r f]
    forall a. Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return []
          else [Constraint' r f] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    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
    forall a. String -> Doc a
    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
    forall a. String -> Doc a
    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
    forall a. Doc a -> Doc a -> Doc a
    <+> Cmp -> Doc
    forall a. Pretty a => a -> Doc
    pretty Cmp
    cmp Doc -> Doc -> Doc
    forall a. Doc a -> Doc a -> Doc a
    <+> 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 r
    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 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)

    -- | Identifiers for rigid variables.
    data NamedRigid = NamedRigid
      { NamedRigid -> String
    rigidName  :: String   -- ^ Name for printing in debug messages.
      , NamedRigid -> Int
    rigidIndex :: Int      -- ^ De Bruijn index.
      } deriving (Int -> NamedRigid -> ShowS
    [NamedRigid] -> ShowS
    NamedRigid -> String
    (Int -> NamedRigid -> ShowS)
    -> (NamedRigid -> String)
    -> ([NamedRigid] -> ShowS)
    -> Show NamedRigid
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> NamedRigid -> ShowS
    showsPrec :: Int -> NamedRigid -> ShowS
    $cshow :: NamedRigid -> String
    show :: NamedRigid -> String
    $cshowList :: [NamedRigid] -> ShowS
    showList :: [NamedRigid] -> ShowS
    Show, (forall x. NamedRigid -> Rep NamedRigid x)
    -> (forall x. Rep NamedRigid x -> NamedRigid) -> Generic NamedRigid
    forall x. Rep NamedRigid x -> NamedRigid
    forall x. NamedRigid -> Rep NamedRigid x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. NamedRigid -> Rep NamedRigid x
    from :: forall x. NamedRigid -> Rep NamedRigid x
    $cto :: forall x. Rep NamedRigid x -> NamedRigid
    to :: forall x. Rep NamedRigid x -> NamedRigid
    Generic)

    instance NFData NamedRigid

    instance Eq NamedRigid where
      == :: NamedRigid -> NamedRigid -> Bool
    (==) = Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (Int -> Int -> Bool)
    -> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` NamedRigid -> Int
    rigidIndex

    instance Ord NamedRigid where
      compare :: NamedRigid -> NamedRigid -> Ordering
    compare = Int -> Int -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Int -> Int -> Ordering)
    -> (NamedRigid -> Int) -> NamedRigid -> NamedRigid -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` NamedRigid -> Int
    rigidIndex

    instance Pretty NamedRigid where
      pretty :: NamedRigid -> Doc
    pretty = String -> Doc
    forall a. String -> Doc a
    P.text (String -> Doc) -> (NamedRigid -> String) -> NamedRigid -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . NamedRigid -> String
    rigidName

    instance Plus NamedRigid Int NamedRigid where
      plus :: NamedRigid -> Int -> NamedRigid
    plus (NamedRigid String
    x Int
    i) Int
    j = String -> Int -> NamedRigid
    NamedRigid String
    x (Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    j)

    -- | Size metas in size expressions.
    data SizeMeta = SizeMeta
      { SizeMeta -> MetaId
    sizeMetaId   :: MetaId
      -- TODO to fix issue 300?
      -- , sizeMetaPerm :: Permutation -- ^ Permutation from the current context
      --                               --   to the context of the meta.
      , SizeMeta -> [Int]
    sizeMetaArgs :: [Int]       -- ^ De Bruijn indices.
      } deriving (Int -> SizeMeta -> ShowS
    [SizeMeta] -> ShowS
    SizeMeta -> String
    (Int -> SizeMeta -> ShowS)
    -> (SizeMeta -> String) -> ([SizeMeta] -> ShowS) -> Show SizeMeta
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> SizeMeta -> ShowS
    showsPrec :: Int -> SizeMeta -> ShowS
    $cshow :: SizeMeta -> String
    show :: SizeMeta -> String
    $cshowList :: [SizeMeta] -> ShowS
    showList :: [SizeMeta] -> ShowS
    Show, (forall x. SizeMeta -> Rep SizeMeta x)
    -> (forall x. Rep SizeMeta x -> SizeMeta) -> Generic SizeMeta
    forall x. Rep SizeMeta x -> SizeMeta
    forall x. SizeMeta -> Rep SizeMeta x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. SizeMeta -> Rep SizeMeta x
    from :: forall x. SizeMeta -> Rep SizeMeta x
    $cto :: forall x. Rep SizeMeta x -> SizeMeta
    to :: forall x. Rep SizeMeta x -> SizeMeta
    Generic)

    instance NFData SizeMeta

    -- | An equality which ignores the meta arguments.
    instance Eq  SizeMeta where
      == :: SizeMeta -> SizeMeta -> Bool
    (==) = MetaId -> MetaId -> Bool
    forall a. Eq a => a -> a -> Bool
    (==) (MetaId -> MetaId -> Bool)
    -> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Bool
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` SizeMeta -> MetaId
    sizeMetaId

    -- | An order which ignores the meta arguments.
    instance Ord SizeMeta where
      compare :: SizeMeta -> SizeMeta -> Ordering
    compare = MetaId -> MetaId -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (MetaId -> MetaId -> Ordering)
    -> (SizeMeta -> MetaId) -> SizeMeta -> SizeMeta -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` SizeMeta -> MetaId
    sizeMetaId

    instance Pretty SizeMeta where
      pretty :: SizeMeta -> Doc
    pretty = MetaId -> Doc
    forall a. Pretty a => a -> Doc
    P.pretty (MetaId -> Doc) -> (SizeMeta -> MetaId) -> SizeMeta -> Doc
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . SizeMeta -> MetaId
    sizeMetaId

    -- | Size expression with de Bruijn indices.
    type DBSizeExpr = SizeExpr' NamedRigid SizeMeta

    type SizeConstraint = Constraint' NamedRigid SizeMeta

    -- | Size constraint with de Bruijn indices.
    data HypSizeConstraint = HypSizeConstraint
      { HypSizeConstraint -> Context
    sizeContext    :: Context
      , HypSizeConstraint -> [Int]
    sizeHypIds     :: [Nat] -- ^ DeBruijn indices
      , HypSizeConstraint -> [SizeConstraint]
    sizeHypotheses :: [SizeConstraint]  -- ^ Living in @Context@.
      , HypSizeConstraint -> SizeConstraint
    sizeConstraint :: SizeConstraint    -- ^ Living in @Context@.
      }
      deriving (Int -> HypSizeConstraint -> ShowS
    [HypSizeConstraint] -> ShowS
    HypSizeConstraint -> String
    (Int -> HypSizeConstraint -> ShowS)
    -> (HypSizeConstraint -> String)
    -> ([HypSizeConstraint] -> ShowS)
    -> Show HypSizeConstraint
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> HypSizeConstraint -> ShowS
    showsPrec :: Int -> HypSizeConstraint -> ShowS
    $cshow :: HypSizeConstraint -> String
    show :: HypSizeConstraint -> String
    $cshowList :: [HypSizeConstraint] -> ShowS
    showList :: [HypSizeConstraint] -> ShowS
    Show, (forall x. HypSizeConstraint -> Rep HypSizeConstraint x)
    -> (forall x. Rep HypSizeConstraint x -> HypSizeConstraint)
    -> Generic HypSizeConstraint
    forall x. Rep HypSizeConstraint x -> HypSizeConstraint
    forall x. HypSizeConstraint -> Rep HypSizeConstraint x
    forall a.
    (forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
    $cfrom :: forall x. HypSizeConstraint -> Rep HypSizeConstraint x
    from :: forall x. HypSizeConstraint -> Rep HypSizeConstraint x
    $cto :: forall x. Rep HypSizeConstraint x -> HypSizeConstraint
    to :: forall x. Rep HypSizeConstraint x -> HypSizeConstraint
    Generic)

    instance Flexs HypSizeConstraint where
      type FlexOf HypSizeConstraint = SizeMeta
      flexs :: HypSizeConstraint -> Set (FlexOf HypSizeConstraint)
    flexs (HypSizeConstraint Context
    _ [Int]
    _ [SizeConstraint]
    hs SizeConstraint
    c) = [SizeConstraint] -> Set (FlexOf [SizeConstraint])
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs [SizeConstraint]
    hs Set SizeMeta -> Set SizeMeta -> Set SizeMeta
    forall a. Monoid a => a -> a -> a
    `mappend` SizeConstraint -> Set (FlexOf SizeConstraint)
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs SizeConstraint
    c

    instance NFData HypSizeConstraint