    {-# OPTIONS_GHC -Wunused-imports #-}

    module Agda.TypeChecking.SizedTypes.WarshallSolver where

    import Prelude hiding ( null, truncate )

    import Control.Monad

    import Data.Function (on)
    import qualified Data.List as List
    import Data.Maybe
    import Data.Set (Set)
    import qualified Data.Set as Set
    import Data.Map (Map)
    import qualified Data.Map as Map

    import Agda.TypeChecking.Monad.Base (TCM)
    import Agda.TypeChecking.Pretty (PrettyTCM)
    import qualified Agda.TypeChecking.Pretty as P
    import Agda.TypeChecking.SizedTypes.Syntax hiding (CTrans, simplify1)
    import qualified Agda.TypeChecking.SizedTypes.Syntax as S
    import Agda.TypeChecking.SizedTypes.Utils

    import Agda.Utils.Graph.AdjacencyMap.Unidirectional
      (Edge(..), Nodes(..), nodes, computeNodes)
    -- (Edge'(..), allNodes, emptyGraph, insertEdge, graphToList, graphFromList, nodes, lookupEdge, outgoing, incoming, diagonal, transClos)
    import qualified Agda.Utils.Graph.AdjacencyMap.Unidirectional as Graph

    import Agda.Utils.Functor
    import Agda.Utils.Null
    import Agda.Syntax.Common.Pretty

    import Agda.Utils.Impossible

    type Graph r f a = Graph.Graph (Node r f) a
    type Edge' r f a = Graph.Edge  (Node r f) a
    type Key r f = Edge' r f ()
    type Nodes r f = Graph.Nodes (Node r f)
    type LabelledEdge r f = Edge' r f Label

    src :: Edge n e -> n
    src :: forall n e. Edge n e -> n
    src = Edge n e -> n
    forall n e. Edge n e -> n
    Graph.source

    dest :: Edge n e -> n
    dest :: forall n e. Edge n e -> n
    dest = Edge n e -> n
    forall n e. Edge n e -> n
    Graph.target

    lookupEdge :: Ord n => Graph.Graph n e -> n -> n -> Maybe e
    lookupEdge :: forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge Graph n e
    g n
    s n
    t = n -> n -> Graph n e -> Maybe e
    forall n e. Ord n => n -> n -> Graph n e -> Maybe e
    Graph.lookup n
    s n
    t Graph n e
    g

    graphToList :: Graph.Graph n e -> [Edge n e]
    graphToList :: forall n e. Graph n e -> [Edge n e]
    graphToList = Graph n e -> [Edge n e]
    forall n e. Graph n e -> [Edge n e]
    Graph.edges

    graphFromList :: Ord n => [Edge n e] -> Graph.Graph n e
    graphFromList :: forall n e. Ord n => [Edge n e] -> Graph n e
    graphFromList = [Edge n e] -> Graph n e
    forall n e. Ord n => [Edge n e] -> Graph n e
    Graph.fromEdges

    insertEdge :: (Ord n, MeetSemiLattice e, Top e) =>
                  Edge n e -> Graph.Graph n e -> Graph.Graph n e
    insertEdge :: forall n e.
    (Ord n, MeetSemiLattice e, Top e) =>
    Edge n e -> Graph n e -> Graph n e
    insertEdge Edge n e
    e Graph n e
    g
      | e -> Bool
    forall a. Top a => a -> Bool
    isTop (Edge n e -> e
    forall n e. Edge n e -> e
    label Edge n e
    e) = Graph n e
    g
      | Bool
    otherwise       = (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
    forall n e.
    Ord n =>
    (e -> e -> e) -> Edge n e -> Graph n e -> Graph n e
    Graph.insertEdgeWith e -> e -> e
    forall a. MeetSemiLattice a => a -> a -> a
    meet Edge n e
    e Graph n e
    g

    -- | Compute list of edges that start in a given node.
    outgoing :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
    outgoing :: forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> Node r f -> [Edge' r f a]
    outgoing Graph r f a
    g Node r f
    s = Graph r f a -> [Node r f] -> [Edge (Node r f) a]
    forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
    Graph.edgesFrom Graph r f a
    g [Node r f
    s]

    -- | Compute list of edges that target a given node.
    --
    --   Note: expensive for unidirectional graph representations.
    incoming :: (Ord r, Ord f) => Graph r f a -> Node r f -> [Edge' r f a]
    incoming :: forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> Node r f -> [Edge' r f a]
    incoming Graph r f a
    g Node r f
    t = Graph r f a -> [Node r f] -> [Edge (Node r f) a]
    forall n e. Ord n => Graph n e -> [n] -> [Edge n e]
    Graph.edgesTo Graph r f a
    g [Node r f
    t]

    -- | @Set.foldl@ does not exist in legacy versions of the @containers@ package.
    setFoldl :: (b -> a -> b) -> b -> Set a -> b
    setFoldl :: forall b a. (b -> a -> b) -> b -> Set a -> b
    setFoldl b -> a -> b
    step b
    start = (b -> a -> b) -> b -> [a] -> b
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    List.foldl' b -> a -> b
    step b
    start ([a] -> b) -> (Set a -> [a]) -> Set a -> b
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set a -> [a]
    forall a. Set a -> [a]
    Set.toAscList
    -- setFoldl = Set.foldl'

    -- | Floyd-Warshall algorithm.
    transClos :: forall n a . (Ord n, Dioid a) => Graph.Graph n a -> Graph.Graph n a
    transClos :: forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
    transClos Graph n a
    g = (Graph n a -> n -> Graph n a) -> Graph n a -> Set n -> Graph n a
    forall b a. (b -> a -> b) -> b -> Set a -> b
    setFoldl Graph n a -> n -> Graph n a
    step Graph n a
    g (Set n -> Graph n a) -> Set n -> Graph n a
    forall a b. (a -> b) -> a -> b
    $ Nodes n -> Set n
    forall n. Nodes n -> Set n
    allNodes Nodes n
    ns
      where
        ns :: Nodes n
    ns       = Graph n a -> Nodes n
    forall n e. Ord n => Graph n e -> Nodes n
    computeNodes Graph n a
    g
        srcs :: [n]
    srcs     = Set n -> [n]
    forall a. Set a -> [a]
    Set.toAscList (Set n -> [n]) -> Set n -> [n]
    forall a b. (a -> b) -> a -> b
    $ Nodes n -> Set n
    forall n. Nodes n -> Set n
    srcNodes Nodes n
    ns
        dests :: [n]
    dests    = Set n -> [n]
    forall a. Set a -> [a]
    Set.toAscList (Set n -> [n]) -> Set n -> [n]
    forall a b. (a -> b) -> a -> b
    $ Nodes n -> Set n
    forall n. Nodes n -> Set n
    tgtNodes Nodes n
    ns
        -- @step g v@ adds all intermediate edges @u --> w@ via @v@ to @g@
        -- step :: (Ord n, Dioid a) => Graph.Graph n n a -> n -> Graph.Graph n n a
        step :: Graph n a -> n -> Graph n a
    step Graph n a
    g n
    v = (Graph n a -> Edge n a -> Graph n a)
    -> Graph n a -> [Edge n a] -> Graph n a
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((Edge n a -> Graph n a -> Graph n a)
    -> Graph n a -> Edge n a -> Graph n a
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Edge n a -> Graph n a -> Graph n a
    forall n e.
    (Ord n, MeetSemiLattice e, Top e) =>
    Edge n e -> Graph n e -> Graph n e
    insertEdge) Graph n a
    g ([Edge n a] -> Graph n a) -> [Edge n a] -> Graph n a
    forall a b. (a -> b) -> a -> b
    $
          [ n -> n -> a -> Edge n a
    forall n e. n -> n -> e -> Edge n e
    Edge n
    u n
    w (a -> Edge n a) -> a -> Edge n a
    forall a b. (a -> b) -> a -> b
    $ a
    l1 a -> a -> a
    forall a. Dioid a => a -> a -> a
    `compose` a
    l2
            | n
    u <- [n]
    srcs
            , n
    w <- [n]
    dests
            , a
    l1 <- Maybe a -> [a]
    forall a. Maybe a -> [a]
    maybeToList (Maybe a -> [a]) -> Maybe a -> [a]
    forall a b. (a -> b) -> a -> b
    $ Graph n a -> n -> n -> Maybe a
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge Graph n a
    g n
    u n
    v
            , a
    l2 <- Maybe a -> [a]
    forall a. Maybe a -> [a]
    maybeToList (Maybe a -> [a]) -> Maybe a -> [a]
    forall a b. (a -> b) -> a -> b
    $ Graph n a -> n -> n -> Maybe a
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge Graph n a
    g n
    v n
    w
          ]

    -- * Edge weights

    data Weight
      = Offset Offset
      | Infinity
      deriving (Weight -> Weight -> Bool
    (Weight -> Weight -> Bool)
    -> (Weight -> Weight -> Bool) -> Eq Weight
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Weight -> Weight -> Bool
    == :: Weight -> Weight -> Bool
    $c/= :: Weight -> Weight -> Bool
    /= :: Weight -> Weight -> Bool
    Eq, Int -> Weight -> ShowS
    [Weight] -> ShowS
    Weight -> String
    (Int -> Weight -> ShowS)
    -> (Weight -> String) -> ([Weight] -> ShowS) -> Show Weight
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Weight -> ShowS
    showsPrec :: Int -> Weight -> ShowS
    $cshow :: Weight -> String
    show :: Weight -> String
    $cshowList :: [Weight] -> ShowS
    showList :: [Weight] -> ShowS
    Show)

    instance Pretty Weight where
      pretty :: Weight -> Doc
    pretty (Offset Offset
    x) = Offset -> Doc
    forall a. Pretty a => a -> Doc
    pretty Offset
    x
      pretty Weight
    Infinity   = Doc
    "∞"

    instance Ord Weight where
      Weight
    x        <= :: Weight -> Weight -> Bool
    <= Weight
    Infinity = Bool
    True
      Weight
    Infinity <= Weight
    y        = Bool
    False
      Offset Offset
    x <= Offset Offset
    y = Offset
    x Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    y

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

    instance Top Weight where
      top :: Weight
    top  = Weight
    Infinity

    instance Enum Weight where
      succ :: Weight -> Weight
    succ (Offset Offset
    x) = Offset -> Weight
    Offset (Offset -> Offset
    forall a. Enum a => a -> a
    succ Offset
    x)
      succ (Weight
    Infinity) = Weight
    Infinity
      pred :: Weight -> Weight
    pred (Offset Offset
    x) = Offset -> Weight
    Offset (Offset -> Offset
    forall a. Enum a => a -> a
    pred Offset
    x)
      pred (Weight
    Infinity) = Weight
    Infinity
      toEnum :: Int -> Weight
    toEnum = Offset -> Weight
    Offset (Offset -> Weight) -> (Int -> Offset) -> Int -> Weight
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Int -> Offset
    forall a. Enum a => Int -> a
    toEnum
      fromEnum :: Weight -> Int
    fromEnum (Offset Offset
    x) = Offset -> Int
    forall a. Enum a => a -> Int
    fromEnum Offset
    x
      fromEnum (Weight
    Infinity) = Int
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Partial implementation of @Num@.
    instance Num Weight where
      Weight
    Infinity + :: Weight -> Weight -> Weight
    + Weight
    y        = Weight
    Infinity
      Weight
    x + Weight
    Infinity        = Weight
    Infinity
      Offset Offset
    x + Offset Offset
    y = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset
    x Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    y
      Weight
    Infinity - :: Weight -> Weight -> Weight
    - Offset Offset
    y = Weight
    Infinity
      Offset Offset
    x - Offset Offset
    y = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset
    x Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    y
      Weight
    x        - Weight
    Infinity = Weight
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      abs :: Weight -> Weight
    abs (Offset Offset
    x)      = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. Num a => a -> a
    abs Offset
    x
      abs Weight
    Infinity        = Weight
    Infinity
      signum :: Weight -> Weight
    signum (Offset Offset
    x)   = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. Num a => a -> a
    signum Offset
    x
      signum Weight
    Infinity     = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset
    1
      fromInteger :: Integer -> Weight
    fromInteger Integer
    x       = Offset -> Weight
    Offset (Integer -> Offset
    forall a. Num a => Integer -> a
    fromInteger Integer
    x)
      Weight
    x * :: Weight -> Weight -> Weight
    * Weight
    y = Weight
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    instance Plus Weight Offset Weight where
      plus :: Weight -> Offset -> Weight
    plus Weight
    w Offset
    k = Weight
    w Weight -> Weight -> Weight
    forall a. Num a => a -> a -> a
    + (Offset -> Weight
    Offset Offset
    k)

    -- | Test for negativity, used to detect negative cycles.
    class Negative a where
      negative :: a -> Bool

    {- leads to Undecidable/OverlappingInstances:
    instance (Ord a, Num a) => Negative a where
      negative = (< 0)
    -}

    instance Negative Int where
      negative :: Int -> Bool
    negative = (Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    < Int
    0)

    instance Negative Offset where
      negative :: Offset -> Bool
    negative (O Int
    x) = Int -> Bool
    forall a. Negative a => a -> Bool
    negative Int
    x

    instance Negative Weight where
      negative :: Weight -> Bool
    negative Weight
    Infinity = Bool
    False
      negative (Offset Offset
    x) = Offset -> Bool
    forall a. Negative a => a -> Bool
    negative Offset
    x

    -- * Edge labels

    -- | Going from @Lt@ to @Le@ is @pred@, going from @Le@ to @Lt@ is @succ@.
    --
    --   @X --(R,n)--> Y@
    --   means  @X (R) Y + n@.
    --   [                      ... if @n@ positive
    --     and    @X + (-n) (R) Y@  if @n@ negative. ]
    data Label
      = Label { Label -> Cmp
    lcmp :: Cmp, Label -> Offset
    loffset :: Offset }
      | LInf  -- ^ Nodes not connected.
      deriving (Int -> Label -> ShowS
    [Label] -> ShowS
    Label -> String
    (Int -> Label -> ShowS)
    -> (Label -> String) -> ([Label] -> ShowS) -> Show Label
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Label -> ShowS
    showsPrec :: Int -> Label -> ShowS
    $cshow :: Label -> String
    show :: Label -> String
    $cshowList :: [Label] -> ShowS
    showList :: [Label] -> ShowS
    Show)

    -- | Convert a label to a weight, decrementing in case of 'Lt'.
    toWeight :: Label -> Weight
    toWeight :: Label -> Weight
    toWeight (Label Cmp
    Le Offset
    w) = Offset -> Weight
    Offset Offset
    w
    toWeight (Label Cmp
    Lt Offset
    w) = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. Enum a => a -> a
    pred Offset
    w
    toWeight Label
    LInf         = Weight
    Infinity

    instance Negative Label where
      negative :: Label -> Bool
    negative = Weight -> Bool
    forall a. Negative a => a -> Bool
    negative (Weight -> Bool) -> (Label -> Weight) -> Label -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Label -> Weight
    toWeight

    instance Eq Label where
      Label Cmp
    cmp Offset
    w == :: Label -> Label -> Bool
    == Label Cmp
    cmp' Offset
    w' = Cmp
    cmp Cmp -> Cmp -> Bool
    forall a. Eq a => a -> a -> Bool
    == Cmp
    cmp' Bool -> Bool -> Bool
    && Offset
    w Offset -> Offset -> Bool
    forall a. Eq a => a -> a -> Bool
    == Offset
    w'
      Label
    LInf        == Label
    LInf          = Bool
    True
      Label
    _           == Label
    _             = Bool
    False

    instance Ord Label where
      Label Cmp
    Lt  Offset
    w <= :: Label -> Label -> Bool
    <= Label Cmp
    Lt Offset
    w' = Offset
    w Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    w'
      Label Cmp
    Le  Offset
    w <= Label Cmp
    Le Offset
    w' = Offset
    w Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    w'
      Label Cmp
    Lt  Offset
    w <= Label Cmp
    Le Offset
    w' = Offset -> Offset
    forall a. Enum a => a -> a
    pred Offset
    w Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    w'
      Label Cmp
    Le  Offset
    w <= Label Cmp
    Lt Offset
    w' = Offset -> Offset
    forall a. Enum a => a -> a
    succ Offset
    w Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    w'
      Label
    _           <= Label
    LInf        = Bool
    True
      LInf{}      <= Label{}     = Bool
    False

    instance Pretty Label where
      pretty :: Label -> Doc
    pretty (Label Cmp
    cmp Offset
    w) = Cmp -> Doc
    forall a. Pretty a => a -> Doc
    pretty Cmp
    cmp Doc -> Doc -> Doc
    forall a. Semigroup a => a -> a -> a
    <> Offset -> Doc
    forall a. Pretty a => a -> Doc
    pretty Offset
    w
      pretty Label
    LInf          = Doc
    "∞"

    instance MeetSemiLattice Label where
      -- one label is neutral
      Label
    LInf       meet :: Label -> Label -> Label
    `meet` Label
    l           = Label
    l
      Label
    l          `meet` Label
    LInf        = Label
    l
      -- other cases
      Label Cmp
    Lt Offset
    w `meet` Label Cmp
    Lt Offset
    w' = Cmp -> Offset -> Label
    Label Cmp
    Lt (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset
    w      Offset -> Offset -> Offset
    forall a. MeetSemiLattice a => a -> a -> a
    `meet` Offset
    w'
      Label Cmp
    Le Offset
    w `meet` Label Cmp
    Le Offset
    w' = Cmp -> Offset -> Label
    Label Cmp
    Le (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset
    w      Offset -> Offset -> Offset
    forall a. MeetSemiLattice a => a -> a -> a
    `meet` Offset
    w'
      Label Cmp
    Lt Offset
    w `meet` Label Cmp
    Le Offset
    w' = Cmp -> Offset -> Label
    Label Cmp
    Lt (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $      Offset
    w Offset -> Offset -> Offset
    forall a. MeetSemiLattice a => a -> a -> a
    `meet` Offset -> Offset
    forall a. Enum a => a -> a
    succ Offset
    w'
      Label Cmp
    Le Offset
    w `meet` Label Cmp
    Lt Offset
    w' = Cmp -> Offset -> Label
    Label Cmp
    Lt (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. Enum a => a -> a
    succ Offset
    w Offset -> Offset -> Offset
    forall a. MeetSemiLattice a => a -> a -> a
    `meet` Offset
    w'

    instance Top Label where
      top :: Label
    top                 = Label
    LInf
      isTop :: Label -> Bool
    isTop Label{}       = Bool
    False
      isTop Label
    LInf          = Bool
    True

    -- * Semiring with idempotent '+' == dioid

    instance Dioid Weight where
      compose :: Weight -> Weight -> Weight
    compose     = Weight -> Weight -> Weight
    forall a. Num a => a -> a -> a
    (+)
      unitCompose :: Weight
    unitCompose = Weight
    0

    instance Dioid Label where
      compose :: Label -> Label -> Label
    compose (Label Cmp
    Lt Offset
    w) (Label Cmp
    Lt Offset
    w')    = Cmp -> Offset -> Label
    Label Cmp
    Lt (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset
    forall a. Enum a => a -> a
    pred (Offset -> Offset) -> Offset -> Offset
    forall a b. (a -> b) -> a -> b
    $ Offset
    w Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    w'
      compose (Label Cmp
    cmp Offset
    w) (Label Cmp
    cmp' Offset
    w') = Cmp -> Offset -> Label
    Label (Cmp -> Cmp -> Cmp
    forall a. Dioid a => a -> a -> a
    compose Cmp
    cmp Cmp
    cmp') (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset
    w Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    + Offset
    w'
      compose Label
    _             Label
    LInf            = Label
    LInf
      compose Label
    LInf          Label
    _               = Label
    LInf
      unitCompose :: Label
    unitCompose = Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0

    -- * Graphs

    -- ** Nodes

    data Node rigid flex
      = NodeZero
      | NodeInfty
      | NodeRigid rigid
      | NodeFlex  flex
      deriving (Int -> Node rigid flex -> ShowS
    [Node rigid flex] -> ShowS
    Node rigid flex -> String
    (Int -> Node rigid flex -> ShowS)
    -> (Node rigid flex -> String)
    -> ([Node rigid flex] -> ShowS)
    -> Show (Node rigid flex)
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> Node rigid flex -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    [Node rigid flex] -> ShowS
    forall rigid flex.
    (Show rigid, Show flex) =>
    Node rigid flex -> String
    $cshowsPrec :: forall rigid flex.
    (Show rigid, Show flex) =>
    Int -> Node rigid flex -> ShowS
    showsPrec :: Int -> Node rigid flex -> ShowS
    $cshow :: forall rigid flex.
    (Show rigid, Show flex) =>
    Node rigid flex -> String
    show :: Node rigid flex -> String
    $cshowList :: forall rigid flex.
    (Show rigid, Show flex) =>
    [Node rigid flex] -> ShowS
    showList :: [Node rigid flex] -> ShowS
    Show, Node rigid flex -> Node rigid flex -> Bool
    (Node rigid flex -> Node rigid flex -> Bool)
    -> (Node rigid flex -> Node rigid flex -> Bool)
    -> Eq (Node rigid flex)
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    forall rigid flex.
    (Eq rigid, Eq flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    $c== :: forall rigid flex.
    (Eq rigid, Eq flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    == :: Node rigid flex -> Node rigid flex -> Bool
    $c/= :: forall rigid flex.
    (Eq rigid, Eq flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    /= :: Node rigid flex -> Node rigid flex -> Bool
    Eq, Eq (Node rigid flex)
    Eq (Node rigid flex) =>
    (Node rigid flex -> Node rigid flex -> Ordering)
    -> (Node rigid flex -> Node rigid flex -> Bool)
    -> (Node rigid flex -> Node rigid flex -> Bool)
    -> (Node rigid flex -> Node rigid flex -> Bool)
    -> (Node rigid flex -> Node rigid flex -> Bool)
    -> (Node rigid flex -> Node rigid flex -> Node rigid flex)
    -> (Node rigid flex -> Node rigid flex -> Node rigid flex)
    -> Ord (Node rigid flex)
    Node rigid flex -> Node rigid flex -> Bool
    Node rigid flex -> Node rigid flex -> Ordering
    Node rigid flex -> Node rigid flex -> Node 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 (Node rigid flex)
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Ordering
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Node rigid flex
    $ccompare :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Ordering
    compare :: Node rigid flex -> Node rigid flex -> Ordering
    $c< :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    < :: Node rigid flex -> Node rigid flex -> Bool
    $c<= :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    <= :: Node rigid flex -> Node rigid flex -> Bool
    $c> :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    > :: Node rigid flex -> Node rigid flex -> Bool
    $c>= :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Bool
    >= :: Node rigid flex -> Node rigid flex -> Bool
    $cmax :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Node rigid flex
    max :: Node rigid flex -> Node rigid flex -> Node rigid flex
    $cmin :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    Node rigid flex -> Node rigid flex -> Node rigid flex
    min :: Node rigid flex -> Node rigid flex -> Node rigid flex
    Ord)

    instance (Pretty rigid, Pretty flex) => Pretty (Node rigid flex) where
      pretty :: Node rigid flex -> Doc
    pretty Node rigid flex
    NodeZero      = Doc
    "0"
      pretty Node rigid flex
    NodeInfty     = Doc
    "∞"
      pretty (NodeRigid rigid
    x) = rigid -> Doc
    forall a. Pretty a => a -> Doc
    pretty rigid
    x
      pretty (NodeFlex  flex
    x) = flex -> Doc
    forall a. Pretty a => a -> Doc
    pretty flex
    x

    isFlexNode :: Node rigid flex -> Maybe flex
    isFlexNode :: forall rigid flex. Node rigid flex -> Maybe flex
    isFlexNode (NodeFlex flex
    x) = flex -> Maybe flex
    forall a. a -> Maybe a
    Just flex
    x
    isFlexNode Node rigid flex
    _            = Maybe flex
    forall a. Maybe a
    Nothing

    isZeroNode :: Node rigid flex -> Bool
    isZeroNode :: forall rigid flex. Node rigid flex -> Bool
    isZeroNode NodeZero{} = Bool
    True
    isZeroNode Node rigid flex
    _          = Bool
    False

    isInftyNode :: Node rigid flex -> Bool
    isInftyNode :: forall rigid flex. Node rigid flex -> Bool
    isInftyNode NodeInfty{} = Bool
    True
    isInftyNode Node rigid flex
    _           = Bool
    False

    nodeToSizeExpr :: Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr :: forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node rigid flex
    n =
      case Node rigid flex
    n of
        Node rigid flex
    NodeZero    -> Offset -> SizeExpr' rigid flex
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const Offset
    0
        Node rigid flex
    NodeInfty   -> SizeExpr' rigid flex
    forall rigid flex. SizeExpr' rigid flex
    Infty
        NodeRigid rigid
    i -> rigid -> Offset -> SizeExpr' rigid flex
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid rigid
    i Offset
    0
        NodeFlex flex
    x  -> flex -> Offset -> SizeExpr' rigid flex
    forall rigid flex. flex -> Offset -> SizeExpr' rigid flex
    Flex flex
    x Offset
    0

    -- ** Edges

    -- | An edge is negative if its label is.
    instance Negative a => Negative (Edge' r f a) where
      negative :: Edge' r f a -> Bool
    negative = a -> Bool
    forall a. Negative a => a -> Bool
    negative (a -> Bool) -> (Edge' r f a -> a) -> Edge' r f a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Edge' r f a -> a
    forall n e. Edge n e -> e
    label

    instance (Ord r, Ord f, MeetSemiLattice a) => MeetSemiLattice (Edge' r f a) where
      e :: Edge' r f a
    e@(Edge Node r f
    u Node r f
    v a
    l) meet :: Edge' r f a -> Edge' r f a -> Edge' r f a
    `meet` e' :: Edge' r f a
    e'@(Edge Node r f
    u' Node r f
    v' a
    l')
        | Node r f
    u Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    u' Bool -> Bool -> Bool
    && Node r f
    v Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    v' = Node r f -> Node r f -> a -> Edge' r f a
    forall n e. n -> n -> e -> Edge n e
    Edge Node r f
    u Node r f
    v (a -> Edge' r f a) -> a -> Edge' r f a
    forall a b. (a -> b) -> a -> b
    $ a
    l a -> a -> a
    forall a. MeetSemiLattice a => a -> a -> a
    `meet` a
    l'
        | Bool
    otherwise          = Edge' r f a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
           -- error $ show e ++ " `meet` " ++ show e'

    instance (Ord r, Ord f, Top a) => Top (Edge' r f a) where
      top :: Edge' r f a
    top = Edge' r f a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      isTop :: Edge' r f a -> Bool
    isTop Edge' r f a
    e = a -> Bool
    forall a. Top a => a -> Bool
    isTop (Edge' r f a -> a
    forall n e. Edge n e -> e
    label Edge' r f a
    e)

    instance (Ord r, Ord f, Dioid a) => Dioid (Edge' r f a) where
      e :: Edge' r f a
    e@(Edge Node r f
    u Node r f
    v a
    l) compose :: Edge' r f a -> Edge' r f a -> Edge' r f a
    `compose` e' :: Edge' r f a
    e'@(Edge Node r f
    v' Node r f
    w a
    l')
       | Node r f
    v Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    v'    = Node r f -> Node r f -> a -> Edge' r f a
    forall n e. n -> n -> e -> Edge n e
    Edge Node r f
    u Node r f
    w (a -> Edge' r f a) -> a -> Edge' r f a
    forall a b. (a -> b) -> a -> b
    $ a
    l a -> a -> a
    forall a. Dioid a => a -> a -> a
    `compose` a
    l'
       | Bool
    otherwise = Edge' r f a
    forall a. HasCallStack => a
    __IMPOSSIBLE__
          -- error $ show e ++ " `compose` " ++ show e'
      unitCompose :: Edge' r f a
    unitCompose  = Edge' r f a
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- ** Graphs

    -- | A graph forest.
    type Graphs r f a = [Graph r f a]

    emptyGraphs :: Graphs r f a
    emptyGraphs :: forall r f a. Graphs r f a
    emptyGraphs = []

    -- | Split a list of graphs @gs@ into those that mention node @n@ and those that do not.
    --   If @n@ is zero or infinity, we regard it as "not mentioned".
    mentions :: (Ord r, Ord f) => Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    mentions :: forall r f a.
    (Ord r, Ord f) =>
    Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    mentions Node r f
    NodeZero    Graphs r f a
    gs = ([], Graphs r f a
    gs)
    mentions Node r f
    NodeInfty   Graphs r f a
    gs = ([], Graphs r f a
    gs)
    mentions NodeRigid{} Graphs r f a
    gs = ([], Graphs r f a
    gs)
    mentions Node r f
    n           Graphs r f a
    gs = (Graph r f a -> Bool)
    -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    List.partition (Node r f -> Set (Node r f) -> Bool
    forall a. Ord a => a -> Set a -> Bool
    Set.member Node r f
    n (Set (Node r f) -> Bool)
    -> (Graph r f a -> Set (Node r f)) -> Graph r f a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Graph r f a -> Set (Node r f)
    forall n e. Graph n e -> Set n
    nodes) Graphs r f a
    gs

    -- | Add an edge to a graph forest.
    --   Graphs that share a node with the edge are joined.
    addEdge :: (Ord r, Ord f, MeetSemiLattice a, Top a) => Edge' r f a -> Graphs r f a -> Graphs r f a
    addEdge :: forall r f a.
    (Ord r, Ord f, MeetSemiLattice a, Top a) =>
    Edge' r f a -> Graphs r f a -> Graphs r f a
    addEdge e :: Edge' r f a
    e@(Edge Node r f
    src Node r f
    dest a
    l) Graphs r f a
    gs =
      -- Note: If we started from an empty forest
      -- and only added edges via @addEdge@, then
      -- @gsSrc@ and @gsDest@ contain each at most one graph.
      let (Graphs r f a
    gsSrc , Graphs r f a
    gsNotSrc)  = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    forall r f a.
    (Ord r, Ord f) =>
    Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    mentions Node r f
    src  Graphs r f a
    gs
          (Graphs r f a
    gsDest, Graphs r f a
    gsNotDest) = Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    forall r f a.
    (Ord r, Ord f) =>
    Node r f -> Graphs r f a -> (Graphs r f a, Graphs r f a)
    mentions Node r f
    dest Graphs r f a
    gsNotSrc
      in Edge' r f a -> Graph (Node r f) a -> Graph (Node r f) a
    forall n e.
    (Ord n, MeetSemiLattice e, Top e) =>
    Edge n e -> Graph n e -> Graph n e
    insertEdge Edge' r f a
    e ((a -> a -> a) -> Graphs r f a -> Graph (Node r f) a
    forall n e. Ord n => (e -> e -> e) -> [Graph n e] -> Graph n e
    Graph.unionsWith a -> a -> a
    forall a. MeetSemiLattice a => a -> a -> a
    meet (Graphs r f a -> Graph (Node r f) a)
    -> Graphs r f a -> Graph (Node r f) a
    forall a b. (a -> b) -> a -> b
    $ Graphs r f a
    gsSrc Graphs r f a -> Graphs r f a -> Graphs r f a
    forall a. [a] -> [a] -> [a]
    ++ Graphs r f a
    gsDest) Graph (Node r f) a -> Graphs r f a -> Graphs r f a
    forall a. a -> [a] -> [a]
    : Graphs r f a
    gsNotDest

    -- | Reflexive closure.  Add edges @0 -> n -> n -> oo@ for all nodes @n@.
    reflClos :: (Ord r, Ord f, Dioid a) => Set (Node r f) -> Graph r f a -> Graph r f a
    reflClos :: forall r f a.
    (Ord r, Ord f, Dioid a) =>
    Set (Node r f) -> Graph r f a -> Graph r f a
    reflClos Set (Node r f)
    ns Graph r f a
    g = (Graph r f a -> Node r f -> Graph r f a)
    -> Graph r f a -> Set (Node r f) -> Graph r f a
    forall b a. (b -> a -> b) -> b -> Set a -> b
    setFoldl Graph r f a -> Node r f -> Graph r f a
    forall {e} {rigid} {flex}.
    (Dioid e, Ord rigid, Ord flex) =>
    Graph (Node rigid flex) e
    -> Node rigid flex -> Graph (Node rigid flex) e
    step Graph r f a
    g Set (Node r f)
    ns' where
        -- have at least the nodes in @ns@
        ns' :: Set (Node r f)
    ns'      = Graph r f a -> Set (Node r f)
    forall n e. Graph n e -> Set n
    nodes Graph r f a
    g Set (Node r f) -> Set (Node r f) -> Set (Node r f)
    forall a. Ord a => Set a -> Set a -> Set a
    `Set.union` Set (Node r f)
    ns
        -- add the trivial edges for all nodes ns'
        step :: Graph (Node rigid flex) e
    -> Node rigid flex -> Graph (Node rigid flex) e
    step Graph (Node rigid flex) e
    g Node rigid flex
    n = (Graph (Node rigid flex) e
     -> Edge (Node rigid flex) e -> Graph (Node rigid flex) e)
    -> Graph (Node rigid flex) e
    -> [Edge (Node rigid flex) e]
    -> Graph (Node rigid flex) e
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((Edge (Node rigid flex) e
     -> Graph (Node rigid flex) e -> Graph (Node rigid flex) e)
    -> Graph (Node rigid flex) e
    -> Edge (Node rigid flex) e
    -> Graph (Node rigid flex) e
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip Edge (Node rigid flex) e
    -> Graph (Node rigid flex) e -> Graph (Node rigid flex) e
    forall n e.
    (Ord n, MeetSemiLattice e, Top e) =>
    Edge n e -> Graph n e -> Graph n e
    insertEdge) Graph (Node rigid flex) e
    g [Edge (Node rigid flex) e]
    es where
          es :: [Edge (Node rigid flex) e]
    es = [ Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
    forall n e. n -> n -> e -> Edge n e
    Edge Node rigid flex
    forall rigid flex. Node rigid flex
    NodeZero Node rigid flex
    n  e
    forall a. Dioid a => a
    unitCompose
               , Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
    forall n e. n -> n -> e -> Edge n e
    Edge Node rigid flex
    n        Node rigid flex
    n  e
    forall a. Dioid a => a
    unitCompose
               , Node rigid flex -> Node rigid flex -> e -> Edge (Node rigid flex) e
    forall n e. n -> n -> e -> Edge n e
    Edge Node rigid flex
    n Node rigid flex
    forall rigid flex. Node rigid flex
    NodeInfty e
    forall a. Dioid a => a
    unitCompose
               ]

    -- UNUSED
    -- -- | Reflexive-transitive closure.
    -- complete :: (Pretty a, Dioid a) => Graph r f a -> Graph r f a
    -- complete = transClos . reflClos

    -- | A graph is 'negative' if it contains a negative loop (diagonal edge).
    --   Makes sense on transitive graphs.
    instance (Ord r, Ord f, Negative a) => Negative (Graph r f a) where
      negative :: Graph r f a -> Bool
    negative = (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Edge (Node r f) a -> Bool
    forall a. Negative a => a -> Bool
    negative ([Edge (Node r f) a] -> Bool)
    -> (Graph r f a -> [Edge (Node r f) a]) -> Graph r f a -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Graph r f a -> [Edge (Node r f) a]
    forall n e. Ord n => Graph n e -> [Edge n e]
    Graph.diagonal

    instance (Ord r, Ord f, Negative a) => Negative (Graphs r f a) where
      negative :: Graphs r f a -> Bool
    negative = (Graph r f a -> Bool) -> Graphs r f a -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any Graph r f a -> Bool
    forall a. Negative a => a -> Bool
    negative

    -- | @h `implies` g@ if any edge in @g@ between rigids and constants
    --   is implied by a corresponding edge in @h@, which means that
    --   the edge in @g@ carries at most the information of the one in @h@.
    --
    --   Application: Constraint implication: Constraints are compatible
    --   with hypotheses.
    implies :: (Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a, Negative a)
      => Graph r f a -> Graph r f a -> Bool
    -- iterate 'test' over all edges in g
    implies :: forall r f a.
    (Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
     Negative a) =>
    Graph r f a -> Graph r f a -> Bool
    implies Graph r f a
    h Graph r f a
    g = (Edge (Node r f) a -> Bool) -> [Edge (Node r f) a] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all Edge (Node r f) a -> Bool
    test (Graph r f a -> [Edge (Node r f) a]
    forall n e. Graph n e -> [Edge n e]
    graphToList Graph r f a
    g)
      where
        -- NB: doing the @test k l@ before the recursive @b@ gives
        -- opportunity to short-cut the conjunction @&&@.
        -- test :: Key -> a -> Bool
        test :: Edge (Node r f) a -> Bool
    test k :: Edge (Node r f) a
    k@(Edge Node r f
    src Node r f
    dest a
    l)
          | Node r f -> Bool
    forall rigid flex. Node rigid flex -> Bool
    isZeroNode Node r f
    src, Bool -> Bool
    not (a -> Bool
    forall a. Negative a => a -> Bool
    negative a
    l) = Bool
    True
          | Node r f -> Bool
    forall rigid flex. Node rigid flex -> Bool
    isInftyNode Node r f
    dest                 = Bool
    True
          | Maybe f -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe f -> Bool) -> Maybe f -> Bool
    forall a b. (a -> b) -> a -> b
    $ Node r f -> Maybe f
    forall rigid flex. Node rigid flex -> Maybe flex
    isFlexNode Node r f
    src          = Bool
    True
          | Maybe f -> Bool
    forall a. Maybe a -> Bool
    isJust (Maybe f -> Bool) -> Maybe f -> Bool
    forall a b. (a -> b) -> a -> b
    $ Node r f -> Maybe f
    forall rigid flex. Node rigid flex -> Maybe flex
    isFlexNode Node r f
    dest         = Bool
    True
          | a -> Bool
    forall a. Top a => a -> Bool
    isTop a
    l                          = Bool
    True
          | Bool
    otherwise = case Graph r f a -> Node r f -> Node r f -> Maybe a
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge Graph r f a
    h Node r f
    src Node r f
    dest of
            Maybe a
    Nothing -> Bool
    False
            Just a
    l' ->
              (a
    l' a -> a -> Bool
    forall a. Ord a => a -> a -> Bool
    <= a
    l) Bool -> Bool -> Bool
    || ( String -> Bool -> Bool
    forall a. String -> a -> a
    trace
                               ( String
    "edge " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Edge (Node r f) a -> String
    forall a. Pretty a => a -> String
    prettyShow (a
    l a -> Edge (Node r f) a -> Edge (Node r f) a
    forall a b. a -> Edge (Node r f) b -> Edge (Node r f) a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Edge (Node r f) a
    k)
                                   String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " not implied by "
                                   String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Edge (Node r f) a -> String
    forall a. Pretty a => a -> String
    prettyShow (a
    l' a -> Edge (Node r f) a -> Edge (Node r f) a
    forall a b. a -> Edge (Node r f) b -> Edge (Node r f) a
    forall (f :: * -> *) a b. Functor f => a -> f b -> f a
    <$ Edge (Node r f) a
    k)
                               )
                               (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool
    False
                           )

    -- implies h g = Map.foldlWithKey (\ b k l -> test k l && b) True g
    --   -- NB: doing the @test k l@ before the recursive @b@ gives
    --   -- opportunity to short-cut the conjunction @&&@.
    --   where
    --     -- test :: Key -> a -> Bool
    --     test k@(Edge src dest ()) l
    --       | isZeroNode src, not (negative l) = True
    --       | isInftyNode dest                 = True
    --       | isJust $ isFlexNode src          = True
    --       | isJust $ isFlexNode dest         = True
    --       | isTop l                          = True
    --       | otherwise = case lookupEdge h src dest of
    --         Nothing -> False
    --         Just l' -> if l' <= l then True else
    --           trace ("edge " ++ show (l <$ k) ++ " not implied by " ++ show (l' <$ k)) $
    --             False

    nodeFromSizeExpr :: SizeExpr' rigid flex -> (Node rigid flex, Offset)
    nodeFromSizeExpr :: forall rigid flex.
    SizeExpr' rigid flex -> (Node rigid flex, Offset)
    nodeFromSizeExpr = \case
      Const   Offset
    n -> (Node rigid flex
    forall rigid flex. Node rigid flex
    NodeZero   , Offset
    n)
      Rigid rigid
    i Offset
    n -> (rigid -> Node rigid flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid rigid
    i, Offset
    n)
      Flex  flex
    x Offset
    n -> (flex -> Node rigid flex
    forall rigid flex. flex -> Node rigid flex
    NodeFlex flex
    x , Offset
    n)
      SizeExpr' rigid flex
    Infty     -> (Node rigid flex
    forall rigid flex. Node rigid flex
    NodeInfty  , Offset
    0)

    edgeFromConstraint :: Constraint' rigid flex -> LabelledEdge rigid flex
    edgeFromConstraint :: forall rigid flex.
    Constraint' rigid flex -> LabelledEdge rigid flex
    edgeFromConstraint (Constraint SizeExpr' rigid flex
    lexp Cmp
    cmp SizeExpr' rigid flex
    rexp) =
      let (Node rigid flex
    leftNode , Offset
    n) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
    forall rigid flex.
    SizeExpr' rigid flex -> (Node rigid flex, Offset)
    nodeFromSizeExpr SizeExpr' rigid flex
    lexp
          (Node rigid flex
    rightNode, Offset
    m) = SizeExpr' rigid flex -> (Node rigid flex, Offset)
    forall rigid flex.
    SizeExpr' rigid flex -> (Node rigid flex, Offset)
    nodeFromSizeExpr SizeExpr' rigid flex
    rexp
      in Node rigid flex
    -> Node rigid flex -> Label -> Edge (Node rigid flex) Label
    forall n e. n -> n -> e -> Edge n e
    Edge Node rigid flex
    leftNode Node rigid flex
    rightNode (Cmp -> Offset -> Label
    Label Cmp
    cmp (Offset -> Label) -> Offset -> Label
    forall a b. (a -> b) -> a -> b
    $ Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    n)

    -- | Build a graph from list of simplified constraints.
    graphFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graph rigid flex Label
    graphFromConstraints :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graph rigid flex Label
    graphFromConstraints [Constraint' rigid flex]
    cs =
      let -- convert to edges
          edges :: [LabelledEdge rigid flex]
    edges = (Constraint' rigid flex -> LabelledEdge rigid flex)
    -> [Constraint' rigid flex] -> [LabelledEdge rigid flex]
    forall a b. (a -> b) -> [a] -> [b]
    map Constraint' rigid flex -> LabelledEdge rigid flex
    forall rigid flex.
    Constraint' rigid flex -> LabelledEdge rigid flex
    edgeFromConstraint [Constraint' rigid flex]
    cs
          -- build a graph from the edges
          g :: Graph (Node rigid flex) Label
    g     = (Graph (Node rigid flex) Label
     -> LabelledEdge rigid flex -> Graph (Node rigid flex) Label)
    -> Graph (Node rigid flex) Label
    -> [LabelledEdge rigid flex]
    -> Graph (Node rigid flex) Label
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((LabelledEdge rigid flex
     -> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
    -> Graph (Node rigid flex) Label
    -> LabelledEdge rigid flex
    -> Graph (Node rigid flex) Label
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip LabelledEdge rigid flex
    -> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
    forall n e.
    (Ord n, MeetSemiLattice e, Top e) =>
    Edge n e -> Graph n e -> Graph n e
    insertEdge) Graph (Node rigid flex) Label
    forall n e. Graph n e
    Graph.empty [LabelledEdge rigid flex]
    edges
      in  Graph (Node rigid flex) Label
    g

    -- | Build a graph from list of simplified constraints.
    graphsFromConstraints :: (Ord rigid, Ord flex) => [Constraint' rigid flex] -> Graphs rigid flex Label
    graphsFromConstraints :: forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graphs rigid flex Label
    graphsFromConstraints [Constraint' rigid flex]
    cs =
      let -- convert to edges
          edges :: [LabelledEdge rigid flex]
    edges = (Constraint' rigid flex -> LabelledEdge rigid flex)
    -> [Constraint' rigid flex] -> [LabelledEdge rigid flex]
    forall a b. (a -> b) -> [a] -> [b]
    map Constraint' rigid flex -> LabelledEdge rigid flex
    forall rigid flex.
    Constraint' rigid flex -> LabelledEdge rigid flex
    edgeFromConstraint [Constraint' rigid flex]
    cs
          -- get all the flexibles mentioned in constraints
          xs :: [flex]
    xs    = Set flex -> [flex]
    forall a. Set a -> [a]
    Set.toList (Set flex -> [flex]) -> Set flex -> [flex]
    forall a b. (a -> b) -> a -> b
    $ [Constraint' rigid flex] -> Set (FlexOf [Constraint' rigid flex])
    forall a. Flexs a => a -> Set (FlexOf a)
    flexs [Constraint' rigid flex]
    cs
          -- for each flexible X, add edges 0 <= X and X <= oo
          fedges :: [LabelledEdge rigid flex]
    fedges = [[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex])
    -> [[LabelledEdge rigid flex]] -> [LabelledEdge rigid flex]
    forall a b. (a -> b) -> a -> b
    $ [flex]
    -> (flex -> [LabelledEdge rigid flex])
    -> [[LabelledEdge rigid flex]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [flex]
    xs ((flex -> [LabelledEdge rigid flex])
     -> [[LabelledEdge rigid flex]])
    -> (flex -> [LabelledEdge rigid flex])
    -> [[LabelledEdge rigid flex]]
    forall a b. (a -> b) -> a -> b
    $ \ flex
    x ->
            [ Node rigid flex
    -> Node rigid flex -> Label -> LabelledEdge rigid flex
    forall n e. n -> n -> e -> Edge n e
    Edge Node rigid flex
    forall rigid flex. Node rigid flex
    NodeZero (flex -> Node rigid flex
    forall rigid flex. flex -> Node rigid flex
    NodeFlex flex
    x) (Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0)
            , Node rigid flex
    -> Node rigid flex -> Label -> LabelledEdge rigid flex
    forall n e. n -> n -> e -> Edge n e
    Edge (flex -> Node rigid flex
    forall rigid flex. flex -> Node rigid flex
    NodeFlex flex
    x) Node rigid flex
    forall rigid flex. Node rigid flex
    NodeInfty (Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0)
            ]
          -- build a graph from the edges
          gs :: Graphs rigid flex Label
    gs    = (Graphs rigid flex Label
     -> LabelledEdge rigid flex -> Graphs rigid flex Label)
    -> Graphs rigid flex Label
    -> [LabelledEdge rigid flex]
    -> Graphs rigid flex Label
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl ((LabelledEdge rigid flex
     -> Graphs rigid flex Label -> Graphs rigid flex Label)
    -> Graphs rigid flex Label
    -> LabelledEdge rigid flex
    -> Graphs rigid flex Label
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip LabelledEdge rigid flex
    -> Graphs rigid flex Label -> Graphs rigid flex Label
    forall r f a.
    (Ord r, Ord f, MeetSemiLattice a, Top a) =>
    Edge' r f a -> Graphs r f a -> Graphs r f a
    addEdge) Graphs rigid flex Label
    forall r f a. Graphs r f a
    emptyGraphs ([LabelledEdge rigid flex]
    fedges [LabelledEdge rigid flex]
    -> [LabelledEdge rigid flex] -> [LabelledEdge rigid flex]
    forall a. [a] -> [a] -> [a]
    ++ [LabelledEdge rigid flex]
    edges)
      in  Graphs rigid flex Label
    gs

    -- | Error messages produced by the solver.

    type Error = TCM Doc

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

    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
    f Constraint' r f
    c = case CTrans r f -> CTrans r f
    forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    S.simplify1 ((TCMT IO Doc -> Maybe [Constraint' r f])
    -> ([Constraint' r f] -> Maybe [Constraint' r f])
    -> Either (TCMT IO Doc) [Constraint' r f]
    -> Maybe [Constraint' r f]
    forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
    either (Maybe [Constraint' r f] -> TCMT IO Doc -> Maybe [Constraint' r f]
    forall a b. a -> b -> a
    const Maybe [Constraint' r f]
    forall a. Maybe a
    Nothing) [Constraint' r f] -> Maybe [Constraint' r f]
    forall a. a -> Maybe a
    Just (Either (TCMT IO Doc) [Constraint' r f] -> Maybe [Constraint' r f])
    -> CTrans r f -> CTrans r f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . CTrans r f
    f) Constraint' r f
    c of
      Maybe [Constraint' r f]
    Nothing -> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
    forall a b. a -> Either a b
    Left (TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f])
    -> TCMT IO Doc -> Either (TCMT IO Doc) [Constraint' r f]
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc
    "size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> Constraint' r f -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    P.pretty Constraint' r f
    c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> TCMT IO Doc
    "is inconsistent"
      Just [Constraint' r f]
    cs -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall a b. b -> Either a b
    Right [Constraint' r f]
    cs

    -- Build hypotheses graph, complete it, check for negative loops.

    type Hyp = Constraint
    type Hyp' = Constraint'
    type HypGraph r f = Graph r f Label

    hypGraph :: (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
      Set rigid -> [Hyp' rigid flex] -> Either Error (HypGraph rigid flex)
    hypGraph :: forall rigid flex.
    (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
    Set rigid
    -> [Hyp' rigid flex] -> Either (TCMT IO Doc) (HypGraph rigid flex)
    hypGraph Set rigid
    is [Hyp' rigid flex]
    hyps0 = do
      -- get a list of hypothesis from a list of constraints
      hyps <- [[Hyp' rigid flex]] -> [Hyp' rigid flex]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Hyp' rigid flex]] -> [Hyp' rigid flex])
    -> Either (TCMT IO Doc) [[Hyp' rigid flex]]
    -> Either (TCMT IO Doc) [Hyp' rigid flex]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
    -> [Hyp' rigid flex] -> Either (TCMT IO Doc) [[Hyp' rigid flex]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
    -> Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex]
    forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    simplify1 ((Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
     -> Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
    -> (Hyp' rigid flex -> Either (TCMT IO Doc) [Hyp' rigid flex])
    -> Hyp' rigid flex
    -> Either (TCMT IO Doc) [Hyp' rigid flex]
    forall a b. (a -> b) -> a -> b
    $ \ Hyp' rigid flex
    c -> [Hyp' rigid flex] -> Either (TCMT IO Doc) [Hyp' rigid flex]
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Hyp' rigid flex
    c]) [Hyp' rigid flex]
    hyps0
      let g = Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
    forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
    transClos (Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
    -> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
    forall a b. (a -> b) -> a -> b
    $
                Set (Node rigid flex)
    -> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
    forall r f a.
    (Ord r, Ord f, Dioid a) =>
    Set (Node r f) -> Graph r f a -> Graph r f a
    reflClos ((rigid -> Node rigid flex) -> Set rigid -> Set (Node rigid flex)
    forall a b. (a -> b) -> Set a -> Set b
    Set.mapMonotonic rigid -> Node rigid flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid Set rigid
    is) (Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label)
    -> Graph (Node rigid flex) Label -> Graph (Node rigid flex) Label
    forall a b. (a -> b) -> a -> b
    $
                  [Hyp' rigid flex] -> Graph (Node rigid flex) Label
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graph rigid flex Label
    graphFromConstraints [Hyp' rigid flex]
    hyps
      when (negative g) $ Left "size hypotheses graph has negative loop"
      return g

    hypConn :: (Ord r, Ord f) => HypGraph r f -> Node r f -> Node r f -> Label
    -- hypConn hg NodeZero n2  = Label Le 0  -- WRONG: not the best information
    -- hypConn hg n1 NodeInfty = Label Le 0
    hypConn :: forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> Node r f -> Node r f -> Label
    hypConn HypGraph r f
    hg Node r f
    n1 Node r f
    n2
      | Node r f
    n1 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    n2                                = Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0
      | Just Label
    l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge HypGraph r f
    hg Node r f
    n1 Node r f
    n2 = Label
    l
      | Bool
    otherwise                               = Label
    forall a. Top a => a
    top

    simplifyWithHypotheses ::
      (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
      HypGraph rigid flex -> [Constraint' rigid flex] ->
      Either Error [Constraint' rigid flex]
    simplifyWithHypotheses :: forall rigid flex.
    (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
    HypGraph rigid flex
    -> [Constraint' rigid flex]
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    simplifyWithHypotheses HypGraph rigid flex
    hg [Constraint' rigid flex]
    cons = [[Constraint' rigid flex]] -> [Constraint' rigid flex]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat ([[Constraint' rigid flex]] -> [Constraint' rigid flex])
    -> Either (TCMT IO Doc) [[Constraint' rigid flex]]
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Constraint' rigid flex
     -> Either (TCMT IO Doc) [Constraint' rigid flex])
    -> [Constraint' rigid flex]
    -> Either (TCMT IO Doc) [[Constraint' rigid flex]]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM ((Constraint' rigid flex
     -> Either (TCMT IO Doc) [Constraint' rigid flex])
    -> Constraint' rigid flex
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    forall f r. (Pretty f, Pretty r, Eq r) => CTrans r f -> CTrans r f
    simplify1 Constraint' rigid flex
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    test) [Constraint' rigid flex]
    cons
      where
        -- Test whether a constraint is compatible with the hypotheses:
        -- Succeeds, if constraint is implied by hypotheses,
        -- fails otherwise.
        test :: Constraint' rigid flex
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    test Constraint' rigid flex
    c = do
          let Edge Node rigid flex
    n1 Node rigid flex
    n2 Label
    l = Constraint' rigid flex -> Edge (Node rigid flex) Label
    forall rigid flex.
    Constraint' rigid flex -> LabelledEdge rigid flex
    edgeFromConstraint Constraint' rigid flex
    c
              l' :: Label
    l' = HypGraph rigid flex -> Node rigid flex -> Node rigid flex -> Label
    forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> Node r f -> Node r f -> Label
    hypConn HypGraph rigid flex
    hg Node rigid flex
    n1 Node rigid flex
    n2
          -- l' <- lookupEdge hg n1 n2
          Bool -> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Label
    l' Label -> Label -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Label
    l) (Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ())
    -> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> Either (TCMT IO Doc) ()
    forall a b. a -> Either a b
    Left (TCMT IO Doc -> Either (TCMT IO Doc) ())
    -> TCMT IO Doc -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $
            TCMT IO Doc
    "size constraint" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> Constraint' rigid flex -> TCMT IO Doc
    forall (m :: * -> *) a. (Applicative m, Pretty a) => a -> m Doc
    P.pretty Constraint' rigid flex
    c TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+>
            TCMT IO Doc
    "not consistent with size hypotheses"
          [Constraint' rigid flex]
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint' rigid flex
    c]
          -- if (l' <= l) then Just [c] else Nothing

    -- Build constraint graph, complete it, check for negative loops.
    -- Check that hypotheses graph implies constraint graphs (rigids).

    type ConGraph r f = Graph r f Label

    constraintGraph ::
      (Ord r, Ord f, Pretty r, Pretty f) =>
      [Constraint' r f] -> HypGraph r f -> Either Error (ConGraph r f)
    constraintGraph :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f) =>
    [Constraint' r f]
    -> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
    constraintGraph [Constraint' r f]
    cons0 Graph (Node r f) Label
    hg = do
      String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String -> Either (TCMT IO Doc) ())
    -> String -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $ String
    "original constraints cons0 = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Constraint' r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [Constraint' r f]
    cons0
      -- Simplify constraints, ensure they are locally consistent with
      -- hypotheses.
      cons <- Graph (Node r f) Label
    -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall rigid flex.
    (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
    HypGraph rigid flex
    -> [Constraint' rigid flex]
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    simplifyWithHypotheses Graph (Node r f) Label
    hg [Constraint' r f]
    cons0
      traceM $ "simplified constraints cons = " ++ prettyShow cons
      -- Build a transitive graph from constraints.
      let g = Graph (Node r f) Label -> Graph (Node r f) Label
    forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
    transClos (Graph (Node r f) Label -> Graph (Node r f) Label)
    -> Graph (Node r f) Label -> Graph (Node r f) Label
    forall a b. (a -> b) -> a -> b
    $ [Constraint' r f] -> Graph (Node r f) Label
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graph rigid flex Label
    graphFromConstraints [Constraint' r f]
    cons
      traceM $ "transitive graph g = " ++ prettyShow (graphToList g)
      -- Ensure it has no negative loops.
      when (negative g) $ Left $
        "size constraint graph has negative loops"
      -- Ensure it does not constrain the hypotheses.
      unless (hg `implies` g) $ Left $
        "size constraint graph constrains size hypotheses"
      return g

    type ConGraphs r f = Graphs r f Label

    constraintGraphs ::
      (Ord r, Ord f, Pretty r, Pretty f) =>
      [Constraint' r f] -> HypGraph r f -> Either Error ([f], ConGraphs r f)
    constraintGraphs :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f) =>
    [Constraint' r f]
    -> HypGraph r f -> Either (TCMT IO Doc) ([f], ConGraphs r f)
    constraintGraphs [Constraint' r f]
    cons0 ConGraph r f
    hg = do
      String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String -> Either (TCMT IO Doc) ())
    -> String -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $ String
    "original constraints cons0 = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Constraint' r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [Constraint' r f]
    cons0
      -- Simplify constraints, ensure they are locally consistent with
      -- hypotheses.
      cons <- ConGraph r f
    -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall rigid flex.
    (Ord rigid, Ord flex, Pretty rigid, Pretty flex) =>
    HypGraph rigid flex
    -> [Constraint' rigid flex]
    -> Either (TCMT IO Doc) [Constraint' rigid flex]
    simplifyWithHypotheses ConGraph r f
    hg [Constraint' r f]
    cons0
      traceM $ "simplified constraints cons = " ++ prettyShow cons
      -- Build a transitive graph forest from constraints.
      let gs0 = [Constraint' r f] -> [ConGraph r f]
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graphs rigid flex Label
    graphsFromConstraints [Constraint' r f]
    cons
      traceM $ "constraint forest gs0 = " ++ prettyShow (map graphToList gs0)
      let gs1 = (ConGraph r f -> ConGraph r f) -> [ConGraph r f] -> [ConGraph r f]
    forall a b. (a -> b) -> [a] -> [b]
    map ConGraph r f -> ConGraph r f
    forall n a. (Ord n, Dioid a) => Graph n a -> Graph n a
    transClos [ConGraph r f]
    gs0
      traceM $ "transitive forest gs1 = " ++ prettyShow (map graphToList gs1)
      -- Check for flexibles to be set to infinity
      let (xss,gs) = unzip $ map infinityFlexs gs1
          xs       = [[f]] -> [f]
    forall (t :: * -> *) a. Foldable t => t [a] -> [a]
    concat [[f]]
    xss
      unless (null xs) $ do
        traceM $ "flexibles to set to oo = " ++ prettyShow xs
        traceM $ "forest after oo-subst  = " ++ prettyShow (map graphToList gs)
      -- Ensure none has negative loops.
      when (negative gs) $ Left $ "size constraint graph has negative loop"
      traceM $ "we are free of negative loops"
      -- Ensure it does not constrain the hypotheses.
      forM_ gs $ \ ConGraph r f
    g -> Bool -> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (ConGraph r f
    hg ConGraph r f -> ConGraph r f -> Bool
    forall r f a.
    (Ord r, Ord f, Pretty r, Pretty f, Pretty a, Top a, Ord a,
     Negative a) =>
    Graph r f a -> Graph r f a -> Bool
    `implies` ConGraph r f
    g) (Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ())
    -> Either (TCMT IO Doc) () -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $ TCMT IO Doc -> Either (TCMT IO Doc) ()
    forall a b. a -> Either a b
    Left (TCMT IO Doc -> Either (TCMT IO Doc) ())
    -> TCMT IO Doc -> Either (TCMT IO Doc) ()
    forall a b. (a -> b) -> a -> b
    $
        TCMT IO Doc
    "size constraint graph constrains size hypotheses"
      traceM $ "any constraint between rigids is implied by the hypotheses"
      return (xs, gs)

    -- | If we have an edge @X + n <= X@ (with n >= 0), we must set @X = oo@.
    infinityFlexs :: (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
    infinityFlexs :: forall r f. (Ord r, Ord f) => ConGraph r f -> ([f], ConGraph r f)
    infinityFlexs ConGraph r f
    g = ([f]
    infFlexs, [f] -> ConGraph r f -> ConGraph r f
    forall f a. SetToInfty f a => [f] -> a -> a
    setToInfty [f]
    infFlexs ConGraph r f
    g)
      where
        -- get the flexibles that need to be set to infinity
        infFlexs :: [f]
    infFlexs = (Edge (Node r f) Label -> Maybe f)
    -> [Edge (Node r f) Label] -> [f]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Edge (Node r f) Label -> Maybe f
    forall {e} {rigid} {b}.
    Negative e =>
    Edge (Node rigid b) e -> Maybe b
    flexNeg ([Edge (Node r f) Label] -> [f]) -> [Edge (Node r f) Label] -> [f]
    forall a b. (a -> b) -> a -> b
    $ ConGraph r f -> [Edge (Node r f) Label]
    forall n e. Ord n => Graph n e -> [Edge n e]
    Graph.diagonal ConGraph r f
    g
        flexNeg :: Edge (Node rigid b) e -> Maybe b
    flexNeg Edge (Node rigid b) e
    e = do
          Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Edge (Node rigid b) e -> Bool
    forall a. Negative a => a -> Bool
    negative Edge (Node rigid b) e
    e
          Node rigid b -> Maybe b
    forall rigid flex. Node rigid flex -> Maybe flex
    isFlexNode (Edge (Node rigid b) e -> Node rigid b
    forall n e. Edge n e -> n
    src Edge (Node rigid b) e
    e)

    class SetToInfty f a where
      setToInfty :: [f] -> a -> a

    instance (Eq f) => SetToInfty f (Node r f) where
      setToInfty :: [f] -> Node r f -> Node r f
    setToInfty [f]
    xs (NodeFlex f
    x) | f
    x f -> [f] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [f]
    xs = Node r f
    forall rigid flex. Node rigid flex
    NodeInfty
      setToInfty [f]
    xs Node r f
    n = Node r f
    n

    instance (Eq f) => SetToInfty f (Edge' r f a) where
      setToInfty :: [f] -> Edge' r f a -> Edge' r f a
    setToInfty [f]
    xs (Edge Node r f
    n1 Node r f
    n2 a
    l) = Node r f -> Node r f -> a -> Edge' r f a
    forall n e. n -> n -> e -> Edge n e
    Edge ([f] -> Node r f -> Node r f
    forall f a. SetToInfty f a => [f] -> a -> a
    setToInfty [f]
    xs Node r f
    n1) ([f] -> Node r f -> Node r f
    forall f a. SetToInfty f a => [f] -> a -> a
    setToInfty [f]
    xs Node r f
    n2) a
    l

    instance (Ord r, Ord f) => SetToInfty f (ConGraph r f) where
      setToInfty :: [f] -> ConGraph r f -> ConGraph r f
    setToInfty [f]
    xs = [Edge (Node r f) Label] -> ConGraph r f
    forall n e. Ord n => [Edge n e] -> Graph n e
    graphFromList ([Edge (Node r f) Label] -> ConGraph r f)
    -> (ConGraph r f -> [Edge (Node r f) Label])
    -> ConGraph r f
    -> ConGraph r f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Edge (Node r f) Label -> Bool)
    -> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Edge (Node r f) Label -> Bool
    forall {rigid} {flex}. Edge (Node rigid flex) Label -> Bool
    h ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
    -> (ConGraph r f -> [Edge (Node r f) Label])
    -> ConGraph r f
    -> [Edge (Node r f) Label]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Edge (Node r f) Label -> Edge (Node r f) Label)
    -> [Edge (Node r f) Label] -> [Edge (Node r f) Label]
    forall a b. (a -> b) -> [a] -> [b]
    map ([f] -> Edge (Node r f) Label -> Edge (Node r f) Label
    forall f a. SetToInfty f a => [f] -> a -> a
    setToInfty [f]
    xs) ([Edge (Node r f) Label] -> [Edge (Node r f) Label])
    -> (ConGraph r f -> [Edge (Node r f) Label])
    -> ConGraph r f
    -> [Edge (Node r f) Label]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . ConGraph r f -> [Edge (Node r f) Label]
    forall n e. Graph n e -> [Edge n e]
    graphToList
        where
          -- filter out edges @oo + k <= oo@
          h :: Edge (Node rigid flex) Label -> Bool
    h (Edge Node rigid flex
    NodeInfty Node rigid flex
    NodeInfty (Label Cmp
    Le Offset
    _)) = Bool
    False
          h Edge (Node rigid flex) Label
    _ = Bool
    True

    -- * Compute solution from constraint graph.

    instance Plus Offset Weight Weight where
      plus :: Offset -> Weight -> Weight
    plus Offset
    e Weight
    Infinity   = Weight
    Infinity
      plus Offset
    e (Offset Offset
    x) = Offset -> Weight
    Offset (Offset -> Weight) -> Offset -> Weight
    forall a b. (a -> b) -> a -> b
    $ Offset -> Offset -> Offset
    forall a b c. Plus a b c => a -> b -> c
    plus Offset
    e Offset
    x

    instance Plus (SizeExpr' r f) Weight (SizeExpr' r f) where
      plus :: SizeExpr' r f -> Weight -> SizeExpr' r f
    plus SizeExpr' r f
    e Weight
    Infinity   = SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty
      plus SizeExpr' r f
    e (Offset Offset
    x) = SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    plus SizeExpr' r f
    e Offset
    x

    instance Plus (SizeExpr' r f) Label (SizeExpr' r f) where
      plus :: SizeExpr' r f -> Label -> SizeExpr' r f
    plus SizeExpr' r f
    e Label
    l = SizeExpr' r f -> Weight -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    plus SizeExpr' r f
    e (Label -> Weight
    toWeight Label
    l)

    -- | Lower or upper bound for a flexible variable
    type Bound r f = Map f (Set (SizeExpr' r f))

    emptyBound :: Bound r f
    emptyBound :: forall r f. Bound r f
    emptyBound = Map f (Set (SizeExpr' r f))
    forall k a. Map k a
    Map.empty

    data Bounds r f = Bounds
      { forall r f. Bounds r f -> Bound r f
    lowerBounds :: Bound r f
      , forall r f. Bounds r f -> Bound r f
    upperBounds :: Bound r f
      , forall r f. Bounds r f -> Set f
    mustBeFinite :: Set f
        -- ^ These metas are < ∞.
      }

    -- | Compute a lower bound for a flexible from an edge.
    edgeToLowerBound :: LabelledEdge r f -> Maybe (f, SizeExpr' r f)
    edgeToLowerBound :: forall r f. LabelledEdge r f -> Maybe (f, SizeExpr' r f)
    edgeToLowerBound LabelledEdge r f
    e =
      case LabelledEdge r f
    e of
        (Edge Node r f
    n1 Node r f
    n2 Label
    LInf) -> Maybe (f, SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Edge Node r f
    NodeZero (NodeFlex f
    x) (Label Cmp
    Le Offset
    o)) | Offset
    o Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    0 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
    forall a. a -> Maybe a
    Just (f
    x, Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const Offset
    0)
        (Edge Node r f
    NodeZero (NodeFlex f
    x) (Label Cmp
    Lt Offset
    o)) | Offset
    o Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    1 -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
    forall a. a -> Maybe a
    Just (f
    x, Offset -> SizeExpr' r f
    forall rigid flex. Offset -> SizeExpr' rigid flex
    Const Offset
    0)
        (Edge Node r f
    n1 (NodeFlex f
    x) Label
    l) -> (f, SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
    forall a. a -> Maybe a
    Just (f
    x, Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    n1 SizeExpr' r f -> Weight -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` (- (Label -> Weight
    toWeight Label
    l)))
        LabelledEdge r f
    _ -> Maybe (f, SizeExpr' r f)
    forall a. Maybe a
    Nothing

    -- | Compute an upper bound for a flexible from an edge.
    edgeToUpperBound :: LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
    edgeToUpperBound :: forall r f. LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
    edgeToUpperBound LabelledEdge r f
    e =
      case LabelledEdge r f
    e of
        (Edge Node r f
    n1 Node r f
    n2 Label
    LInf) -> Maybe (f, Cmp, SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (Edge Node r f
    n1           Node r f
    NodeInfty (Label Cmp
    Le Offset
    _)) -> Maybe (f, Cmp, SizeExpr' r f)
    forall a. Maybe a
    Nothing
        (Edge (NodeFlex f
    x) Node r f
    NodeInfty (Label Cmp
    Lt Offset
    _)) -> (f, Cmp, SizeExpr' r f) -> Maybe (f, Cmp, SizeExpr' r f)
    forall a. a -> Maybe a
    Just (f
    x, Cmp
    Lt, SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty)
        (Edge (NodeFlex f
    x) Node r f
    n2        Label
    l           ) -> (f, Cmp, SizeExpr' r f) -> Maybe (f, Cmp, SizeExpr' r f)
    forall a. a -> Maybe a
    Just (f
    x, Cmp
    Le, Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    n2 SizeExpr' r f -> Weight -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` (Label -> Weight
    toWeight Label
    l))
        LabelledEdge r f
    _ -> Maybe (f, Cmp, SizeExpr' r f)
    forall a. Maybe a
    Nothing

    -- | Compute the lower bounds for all flexibles in a graph.
    graphToLowerBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
    graphToLowerBounds :: forall r f. (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
    graphToLowerBounds = ((Bound r f -> LabelledEdge r f -> Bound r f)
     -> Bound r f -> [LabelledEdge r f] -> Bound r f)
    -> Bound r f
    -> (Bound r f -> LabelledEdge r f -> Bound r f)
    -> [LabelledEdge r f]
    -> Bound r f
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Bound r f -> LabelledEdge r f -> Bound r f)
    -> Bound r f -> [LabelledEdge r f] -> Bound r f
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl Bound r f
    forall r f. Bound r f
    emptyBound ((Bound r f -> LabelledEdge r f -> Bound r f)
     -> [LabelledEdge r f] -> Bound r f)
    -> (Bound r f -> LabelledEdge r f -> Bound r f)
    -> [LabelledEdge r f]
    -> Bound r f
    forall a b. (a -> b) -> a -> b
    $ \ Bound r f
    bs LabelledEdge r f
    e ->
      case LabelledEdge r f -> Maybe (f, SizeExpr' r f)
    forall r f. LabelledEdge r f -> Maybe (f, SizeExpr' r f)
    edgeToLowerBound LabelledEdge r f
    e of
        Maybe (f, SizeExpr' r f)
    Nothing          -> Bound r f
    bs
        Just (f
    x, Flex{}) -> Bound r f
    bs  -- ignore flexible bounds
        Just (f
    x, SizeExpr' r f
    a)      -> (Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
    -> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union f
    x (SizeExpr' r f -> Set (SizeExpr' r f)
    forall a. a -> Set a
    Set.singleton SizeExpr' r f
    a) Bound r f
    bs

    -- | Compute the upper bounds for all flexibles in a graph.
    graphToUpperBounds :: (Ord r, Ord f) => [LabelledEdge r f] -> (Bound r f, Set f)
    graphToUpperBounds :: forall r f.
    (Ord r, Ord f) =>
    [LabelledEdge r f] -> (Bound r f, Set f)
    graphToUpperBounds = (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
     -> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f))
    -> (Bound r f, Set f)
    -> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
    -> [LabelledEdge r f]
    -> (Bound r f, Set f)
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
    -> (Bound r f, Set f) -> [LabelledEdge r f] -> (Bound r f, Set f)
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (Bound r f
    forall r f. Bound r f
    emptyBound, Set f
    forall a. Set a
    Set.empty) (((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
     -> [LabelledEdge r f] -> (Bound r f, Set f))
    -> ((Bound r f, Set f) -> LabelledEdge r f -> (Bound r f, Set f))
    -> [LabelledEdge r f]
    -> (Bound r f, Set f)
    forall a b. (a -> b) -> a -> b
    $ \ (Bound r f
    bs, Set f
    fs) LabelledEdge r f
    e ->
      case LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
    forall r f. LabelledEdge r f -> Maybe (f, Cmp, SizeExpr' r f)
    edgeToUpperBound LabelledEdge r f
    e of
        Maybe (f, Cmp, SizeExpr' r f)
    Nothing             -> (Bound r f
    bs, Set f
    fs)
        Just (f
    x, Cmp
    _, Flex{}) -> (Bound r f
    bs, Set f
    fs)  -- ignore flexible bounds
        Just (f
    x, Cmp
    Lt, SizeExpr' r f
    Infty) -> (Bound r f
    bs, f -> Set f -> Set f
    forall a. Ord a => a -> Set a -> Set a
    Set.insert f
    x Set f
    fs)
        Just (f
    x, Cmp
    Le, SizeExpr' r f
    a)     -> ((Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f))
    -> f -> Set (SizeExpr' r f) -> Bound r f -> Bound r f
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    Map.insertWith Set (SizeExpr' r f) -> Set (SizeExpr' r f) -> Set (SizeExpr' r f)
    forall a. Ord a => Set a -> Set a -> Set a
    Set.union f
    x (SizeExpr' r f -> Set (SizeExpr' r f)
    forall a. a -> Set a
    Set.singleton SizeExpr' r f
    a) Bound r f
    bs, Set f
    fs)
        Maybe (f, Cmp, SizeExpr' r f)
    _                   -> (Bound r f, Set f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__

    -- | Compute the bounds for all flexibles in a graph.
    bounds :: (Ord r, Ord f) => ConGraph r f -> Bounds r f
    bounds :: forall r f. (Ord r, Ord f) => ConGraph r f -> Bounds r f
    bounds ConGraph r f
    g = Bound r f -> Bound r f -> Set f -> Bounds r f
    forall r f. Bound r f -> Bound r f -> Set f -> Bounds r f
    Bounds Bound r f
    lbs Bound r f
    ubs Set f
    fs
      where edges :: [Edge (Node r f) Label]
    edges     = ConGraph r f -> [Edge (Node r f) Label]
    forall n e. Graph n e -> [Edge n e]
    graphToList ConGraph r f
    g
            lbs :: Bound r f
    lbs       = [Edge (Node r f) Label] -> Bound r f
    forall r f. (Ord r, Ord f) => [LabelledEdge r f] -> Bound r f
    graphToLowerBounds [Edge (Node r f) Label]
    edges
            (Bound r f
    ubs, Set f
    fs) = [Edge (Node r f) Label] -> (Bound r f, Set f)
    forall r f.
    (Ord r, Ord f) =>
    [LabelledEdge r f] -> (Bound r f, Set f)
    graphToUpperBounds [Edge (Node r f) Label]
    edges

    -- | Compute the relative minima in a set of nodes (those that do not have
    --   a predecessor in the set).
    smallest ::(Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
    smallest :: forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> [Node r f] -> [Node r f]
    smallest HypGraph r f
    hg [Node r f]
    ns
      | Node r f
    forall rigid flex. Node rigid flex
    NodeZero Node r f -> [Node r f] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Node r f]
    ns = [Node r f
    forall rigid flex. Node rigid flex
    NodeZero]
      | Bool
    otherwise          = (Node r f -> Bool) -> [Node r f] -> [Node r f]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Node r f -> Bool
    hasNoPred [Node r f]
    ns where
          hasNoPred :: Node r f -> Bool
    hasNoPred Node r f
    NodeInfty = Bool
    False
          hasNoPred Node r f
    n = [()] -> Bool
    forall a. Null a => a -> Bool
    null ([()] -> Bool) -> [()] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Node r f -> Maybe ()) -> [Node r f] -> [()]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Node r f -> Maybe ()
    strictEdge [Node r f]
    ns where
            -- is there an edge n -l-> n' with l <= 0
            strictEdge :: Node r f -> Maybe ()
    strictEdge Node r f
    n' = do
              Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Node r f
    n Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Node r f
    n')  -- exclude loops
              l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge HypGraph r f
    hg Node r f
    n' Node r f
    n
              guard (toWeight l <= 0)
              return ()

    -- | Compute the relative maxima in a set of nodes (those that do not have
    --   a successor in the set).
    largest ::(Ord r, Ord f) => HypGraph r f -> [Node r f] -> [Node r f]
    largest :: forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> [Node r f] -> [Node r f]
    largest HypGraph r f
    hg [Node r f]
    ns
      | Node r f
    forall rigid flex. Node rigid flex
    NodeInfty Node r f -> [Node r f] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Node r f]
    ns = [Node r f
    forall rigid flex. Node rigid flex
    NodeInfty]
      | Bool
    otherwise          = (Node r f -> Bool) -> [Node r f] -> [Node r f]
    forall a. (a -> Bool) -> [a] -> [a]
    filter Node r f -> Bool
    hasNoSucc [Node r f]
    ns where
          hasNoSucc :: Node r f -> Bool
    hasNoSucc Node r f
    NodeZero = Bool
    False
          hasNoSucc Node r f
    n = [()] -> Bool
    forall a. Null a => a -> Bool
    null ([()] -> Bool) -> [()] -> Bool
    forall a b. (a -> b) -> a -> b
    $ (Node r f -> Maybe ()) -> [Node r f] -> [()]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Node r f -> Maybe ()
    strictEdge [Node r f]
    ns where
            -- is there an edge n -l-> n' with l <= 0
            strictEdge :: Node r f -> Maybe ()
    strictEdge Node r f
    n' = do
              Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Node r f
    n Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    /= Node r f
    n')  -- exclude loops
              l <- HypGraph r f -> Node r f -> Node r f -> Maybe Label
    forall n e. Ord n => Graph n e -> n -> n -> Maybe e
    lookupEdge HypGraph r f
    hg Node r f
    n Node r f
    n'
              guard (toWeight l <= 0)
              return ()

    {-|  Given source nodes n1,n2,... find all target nodes m1,m2, such
         that for all j, there are edges  n_i --l_ij--> m_j  for all i.
         Return these edges as a map from target notes to a list of edges.
         We assume the graph is reflexive-transitive.
     -}
    commonSuccs :: (Ord r, Ord f) =>
                   Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonSuccs :: forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonSuccs Graph r f a
    hg [Node r f]
    srcs = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
    forall {k} {a}. Ord k => [Map k [a]] -> Map k [a]
    intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
    -> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
    forall a b. (a -> b) -> a -> b
    $ (Node r f -> Map (Node r f) [Edge' r f a])
    -> [Node r f] -> [Map (Node r f) [Edge' r f a]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
    forall {e}.
    [Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
    buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
    -> (Node r f -> [Edge' r f a])
    -> Node r f
    -> Map (Node r f) [Edge' r f a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Graph r f a -> Node r f -> [Edge' r f a]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> Node r f -> [Edge' r f a]
    outgoing Graph r f a
    hg) [Node r f]
    srcs
      where
       buildmap :: [Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
    buildmap            = ([Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e])
    -> [(Node r f, [Edge (Node r f) e])]
    -> Map (Node r f) [Edge (Node r f) e]
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith [Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(Node r f, [Edge (Node r f) e])]
     -> Map (Node r f) [Edge (Node r f) e])
    -> ([Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])])
    -> [Edge (Node r f) e]
    -> Map (Node r f) [Edge (Node r f) e]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Edge (Node r f) e -> (Node r f, [Edge (Node r f) e]))
    -> [Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Edge (Node r f) e
    e -> (Edge (Node r f) e -> Node r f
    forall n e. Edge n e -> n
    dest Edge (Node r f) e
    e, [Edge (Node r f) e
    e]))
         -- __IMPOSSIBLE__ because it is not a multi-graph; there is at most one egde per (src,dest)
       intersectAll :: [Map k [a]] -> Map k [a]
    intersectAll []     = Map k [a]
    forall k a. Map k a
    Map.empty
       intersectAll (Map k [a]
    m:[Map k [a]]
    ms) = (Map k [a] -> Map k [a] -> Map k [a])
    -> Map k [a] -> [Map k [a]] -> Map k [a]
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    Map.intersectionWith [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    (++)) Map k [a]
    m [Map k [a]]
    ms

    {-|  Given target nodes m1,m2,... find all source nodes n1,n2, such
         that for all j, there are edges  n_i --l_ij--> m_j  for all i.
         Return these edges as a map from target notes to a list of edges.
         We assume the graph is reflexive-transitive.
     -}
    commonPreds :: (Ord r, Ord f) => Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonPreds :: forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonPreds Graph r f a
    hg [Node r f]
    tgts = [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
    forall {k} {a}. Ord k => [Map k [a]] -> Map k [a]
    intersectAll ([Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a])
    -> [Map (Node r f) [Edge' r f a]] -> Map (Node r f) [Edge' r f a]
    forall a b. (a -> b) -> a -> b
    $  (Node r f -> Map (Node r f) [Edge' r f a])
    -> [Node r f] -> [Map (Node r f) [Edge' r f a]]
    forall a b. (a -> b) -> [a] -> [b]
    map ([Edge' r f a] -> Map (Node r f) [Edge' r f a]
    forall {e}.
    [Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
    buildmap ([Edge' r f a] -> Map (Node r f) [Edge' r f a])
    -> (Node r f -> [Edge' r f a])
    -> Node r f
    -> Map (Node r f) [Edge' r f a]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Graph r f a -> Node r f -> [Edge' r f a]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> Node r f -> [Edge' r f a]
    incoming Graph r f a
    hg) [Node r f]
    tgts
      where
       buildmap :: [Edge (Node r f) e] -> Map (Node r f) [Edge (Node r f) e]
    buildmap = ([Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e])
    -> [(Node r f, [Edge (Node r f) e])]
    -> Map (Node r f) [Edge (Node r f) e]
    forall k a. Ord k => (a -> a -> a) -> [(k, a)] -> Map k a
    Map.fromListWith [Edge (Node r f) e] -> [Edge (Node r f) e] -> [Edge (Node r f) e]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ ([(Node r f, [Edge (Node r f) e])]
     -> Map (Node r f) [Edge (Node r f) e])
    -> ([Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])])
    -> [Edge (Node r f) e]
    -> Map (Node r f) [Edge (Node r f) e]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Edge (Node r f) e -> (Node r f, [Edge (Node r f) e]))
    -> [Edge (Node r f) e] -> [(Node r f, [Edge (Node r f) e])]
    forall a b. (a -> b) -> [a] -> [b]
    map (\ Edge (Node r f) e
    e -> (Edge (Node r f) e -> Node r f
    forall n e. Edge n e -> n
    src Edge (Node r f) e
    e, [Edge (Node r f) e
    e]))
       intersectAll :: [Map k [a]] -> Map k [a]
    intersectAll []     = Map k [a]
    forall k a. Map k a
    Map.empty
       intersectAll (Map k [a]
    m:[Map k [a]]
    ms) = (Map k [a] -> Map k [a] -> Map k [a])
    -> Map k [a] -> [Map k [a]] -> Map k [a]
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl (([a] -> [a] -> [a]) -> Map k [a] -> Map k [a] -> Map k [a]
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    Map.intersectionWith [a] -> [a] -> [a]
    forall a. [a] -> [a] -> [a]
    (++)) Map k [a]
    m [Map k [a]]
    ms

    -- | Compute the sup of two different rigids or a rigid and a constant.
    lub'
      :: forall r f . (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
      => HypGraph r f
      -> (Node r f, Offset)
      -> (Node r f, Offset)
      -> Maybe (SizeExpr' r f)
    lub' :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    lub' HypGraph r f
    hg (Node r f
    node1, Offset
    n) (Node r f
    node2, Offset
    m) = do
      let sucs :: Map (Node r f) [Edge' r f Label]
    sucs     = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonSuccs HypGraph r f
    hg [Node r f
    node1, Node r f
    node2]
          sucNodes :: [Node r f]
    sucNodes = HypGraph r f -> [Node r f] -> [Node r f]
    forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> [Node r f] -> [Node r f]
    smallest HypGraph r f
    hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
    forall a b. (a -> b) -> a -> b
    $ Map (Node r f) [Edge' r f Label] -> [Node r f]
    forall k a. Map k a -> [k]
    Map.keys Map (Node r f) [Edge' r f Label]
    sucs
      String -> Maybe ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "lub': sucs = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Map (Node r f) [Edge' r f Label] -> String
    forall a. Show a => a -> String
    show Map (Node r f) [Edge' r f Label]
    sucs) -- FIXME: prettyShow
      case [Node r f]
    sucNodes of
        -- there is a unique smallest common successor n0 of node1 and node2
        [Node r f
    n0] -> do
          -- then there are exactly two edges node1 --l1--> n0 and node2 --l2--> n0
          -- Andreas, 2017-04-28, issue #2558: The following invariant does not hold always
          -- -- with non-positive weights l1, l2
          let es :: [Edge' r f Label]
    es = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
    forall a. a -> Maybe a -> a
    fromMaybe [Edge' r f Label]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
    -> Maybe [Edge' r f Label] -> [Edge' r f Label]
    forall a b. (a -> b) -> a -> b
    $ Node r f
    -> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Node r f
    n0 Map (Node r f) [Edge' r f Label]
    sucs
          case [Edge' r f Label]
    es of
            [ Edge Node r f
    node1x Node r f
    n1 Label
    l1 ,
              Edge Node r f
    node2x Node r f
    n2 Label
    l2 ] -> do
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    n0 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    n1)         Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    n0 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    n2)         Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    node1 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    node1x)  Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    node2 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    node2x)  Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              -- Andreas, 2017-04-28, issue #2558: The following invariant does not hold always
              -- unless (toWeight l1 <= 0) __IMPOSSIBLE__
              -- unless (toWeight l2 <= 0) __IMPOSSIBLE__
              let o :: Weight
                  o :: Weight
    o = Weight -> Weight -> Weight
    forall a. Ord a => a -> a -> a
    max (Offset
    n Offset -> Weight -> Weight
    forall a b c. Plus a b c => a -> b -> c
    `plus` Label -> Weight
    toWeight Label
    l1) (Offset
    m Offset -> Weight -> Weight
    forall a b c. Plus a b c => a -> b -> c
    `plus` Label -> Weight
    toWeight Label
    l2)
              SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    n0 SizeExpr' r f -> Weight -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Weight
    o
            [Edge' r f Label]
    _ -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- otherwise, we cannot compute the sup
        [Node r f]
    _ -> do
          let SizeExpr' r f
    a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    node1 SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Offset
    n
          let SizeExpr' r f
    a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    node2 SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Offset
    m
          String -> Maybe ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "cannot compute lub of " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    a1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " and " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    a2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " because sucNodes = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Node r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [Node r f]
    sucNodes)
          Maybe (SizeExpr' r f)
    forall a. Maybe a
    Nothing

    -- | Compute the inf of two different rigids or a rigid and a constant.
    glb'
      :: forall r f . (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
      => HypGraph r f
      -> (Node r f, Offset)
      -> (Node r f, Offset)
      -> Maybe (SizeExpr' r f)
    glb' :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    glb' HypGraph r f
    hg (Node r f
    node1, Offset
    n) (Node r f
    node2, Offset
    m) = do
      let preds :: Map (Node r f) [Edge' r f Label]
    preds     = HypGraph r f -> [Node r f] -> Map (Node r f) [Edge' r f Label]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonPreds HypGraph r f
    hg [Node r f
    node1, Node r f
    node2]
          predNodes :: [Node r f]
    predNodes = HypGraph r f -> [Node r f] -> [Node r f]
    forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> [Node r f] -> [Node r f]
    largest HypGraph r f
    hg ([Node r f] -> [Node r f]) -> [Node r f] -> [Node r f]
    forall a b. (a -> b) -> a -> b
    $ Map (Node r f) [Edge' r f Label] -> [Node r f]
    forall k a. Map k a -> [k]
    Map.keys Map (Node r f) [Edge' r f Label]
    preds
      String -> Maybe ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "glb': preds = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ Map (Node r f) [Edge' r f Label] -> String
    forall a. Show a => a -> String
    show Map (Node r f) [Edge' r f Label]
    preds) -- FIXME: prettyShow
      case [Node r f]
    predNodes of
        -- there is a unique greatest common predecessor n0 of node1 and node2
        [Node r f
    n0] -> do
          -- then there are exactly two edges n0 --l1--> node1 and n0 --l2--> node2
          -- Andreas, 2017-04-28, issue #2558: The following invariant may not hold always
          -- -- with non-positive weigths l1, l2
          let es :: [Edge' r f Label]
    es = [Edge' r f Label] -> Maybe [Edge' r f Label] -> [Edge' r f Label]
    forall a. a -> Maybe a -> a
    fromMaybe [Edge' r f Label]
    forall a. HasCallStack => a
    __IMPOSSIBLE__ (Maybe [Edge' r f Label] -> [Edge' r f Label])
    -> Maybe [Edge' r f Label] -> [Edge' r f Label]
    forall a b. (a -> b) -> a -> b
    $ Node r f
    -> Map (Node r f) [Edge' r f Label] -> Maybe [Edge' r f Label]
    forall k a. Ord k => k -> Map k a -> Maybe a
    Map.lookup Node r f
    n0 Map (Node r f) [Edge' r f Label]
    preds
          case [Edge' r f Label]
    es of
            [ Edge Node r f
    n1 Node r f
    node1x Label
    l1 ,
              Edge Node r f
    n2 Node r f
    node2x Label
    l2] -> do
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    n0 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    n1)         Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    n0 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    n2)         Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    node1 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    node1x)  Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              Bool -> Maybe () -> Maybe ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (Node r f
    node2 Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    node2x)  Maybe ()
    forall a. HasCallStack => a
    __IMPOSSIBLE__
              -- Andreas, 2017-04-28, issue #2558: The following invariant may not hold always
              -- unless (toWeight l1 <= 0) __IMPOSSIBLE__
              -- unless (toWeight l2 <= 0) __IMPOSSIBLE__
              let o :: Weight
                  o :: Weight
    o = Weight -> Weight -> Weight
    forall a. Ord a => a -> a -> a
    max (Offset
    n Offset -> Weight -> Weight
    forall a b c. Plus a b c => a -> b -> c
    `plus` Label -> Weight
    toWeight Label
    l1) (Offset
    m Offset -> Weight -> Weight
    forall a b c. Plus a b c => a -> b -> c
    `plus` Label -> Weight
    toWeight Label
    l2)
              SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    n0 SizeExpr' r f -> Weight -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Weight
    o
            [Edge' r f Label]
    _ -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        -- otherwise, we cannot compute the sup
        [Node r f]
    _ -> do
          let SizeExpr' r f
    a1 :: SizeExpr' r f = Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    node1 SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Offset
    n
          let SizeExpr' r f
    a2 :: SizeExpr' r f = Node r f -> SizeExpr' r f
    forall rigid flex. Node rigid flex -> SizeExpr' rigid flex
    nodeToSizeExpr Node r f
    node2 SizeExpr' r f -> Offset -> SizeExpr' r f
    forall a b c. Plus a b c => a -> b -> c
    `plus` Offset
    m
          String -> Maybe ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "cannot compute glb of " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    a1 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " and " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    a2 String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    " because predNodes = " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [Node r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [Node r f]
    predNodes)
          Maybe (SizeExpr' r f)
    forall a. Maybe a
    Nothing

    -- | Compute the least upper bound (sup).
    lub
      :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
      => HypGraph r f
      -> SizeExpr' r f
      -> SizeExpr' r f
      -> Maybe (SizeExpr' r f)
    lub :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    lub HypGraph r f
    hg SizeExpr' r f
    a1 SizeExpr' r f
    a2 =
      case (SizeExpr' r f
    a1, SizeExpr' r f
    a2) of
        (Flex{}, SizeExpr' r f
    _)   -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (SizeExpr' r f
    _, Flex{})   -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (SizeExpr' r f
    Infty, SizeExpr' r f
    a2)   -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty
        (SizeExpr' r f
    a1, SizeExpr' r f
    Infty)   -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    forall rigid flex. SizeExpr' rigid flex
    Infty
        (Const Offset
    n  , Const Offset
    m  )
                      -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Offset
    forall a. Ord a => a -> a -> a
    max Offset
    n Offset
    m
        (Const Offset
    n  , Rigid r
    j Offset
    m)
          | Offset
    m Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    n    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a2
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    lub' HypGraph r f
    hg (Node r f
    forall rigid flex. Node rigid flex
    NodeZero, Offset
    n) (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    j, Offset
    m)
        (Rigid r
    i Offset
    n, Const Offset
    m  )
          | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Offset
    m    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a1
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    lub' HypGraph r f
    hg (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i, Offset
    n) (Node r f
    forall rigid flex. Node rigid flex
    NodeZero, Offset
    m)
        (Rigid r
    i Offset
    n, Rigid r
    j Offset
    m)
          | r
    i r -> r -> Bool
    forall a. Eq a => a -> a -> Bool
    == r
    j    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Offset
    forall a. Ord a => a -> a -> a
    max Offset
    n Offset
    m
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    lub' HypGraph r f
    hg (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i, Offset
    n) (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    j, Offset
    m)

    {- Finding the glb of two rigid size expressions in hypotheses graph

      a1 = Rigid i n
      a2 = Rigid j m

      Find the topological predecessors of (NodeRigid i)
      Find the topological predecessors of (NodeRigid j)

    -}

    -- | Compute the greatest lower bound (inf) of size expressions relative
    --   to a hypotheses graph.
    glb
      :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
      => HypGraph r f
      -> SizeExpr' r f
      -> SizeExpr' r f
      -> Maybe (SizeExpr' r f)
    glb :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    glb HypGraph r f
    hg SizeExpr' r f
    a1 SizeExpr' r f
    a2 =
      case (SizeExpr' r f
    a1, SizeExpr' r f
    a2) of
        (Flex{}, SizeExpr' r f
    _) -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (SizeExpr' r f
    _, Flex{}) -> Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
        (SizeExpr' r f
    Infty, SizeExpr' r f
    a2) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a2
        (SizeExpr' r f
    a1, SizeExpr' r f
    Infty) -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a1
        (Const Offset
    n  , Const Offset
    m  )          -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Offset
    forall a. Ord a => a -> a -> a
    min Offset
    n Offset
    m
        (Const Offset
    n  , Rigid r
    i Offset
    m)
          | Offset
    n Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    m    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a1
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    glb' HypGraph r f
    hg (Node r f
    forall rigid flex. Node rigid flex
    NodeZero, Offset
    n) (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i, Offset
    m)
        (Rigid r
    i Offset
    n, Const Offset
    m  )
          | Offset
    m Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    n    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    a2
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    glb' HypGraph r f
    hg (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i, Offset
    n) (Node r f
    forall rigid flex. Node rigid flex
    NodeZero, Offset
    m)
        (Rigid r
    i Offset
    n, Rigid r
    j Offset
    m)
          | r
    i r -> r -> Bool
    forall a. Eq a => a -> a -> Bool
    == r
    j    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ 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 -> Offset
    forall a. Ord a => a -> a -> a
    min Offset
    n Offset
    m
          | Bool
    otherwise -> HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Maybe (SizeExpr' r f)
    glb' HypGraph r f
    hg (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i, Offset
    n) (r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    j, Offset
    m)
    {-
        (Rigid i n, Rigid j m) -> do
          let iLeqj = Map.lookup (Edge (NodeRigid i) (NodeRigid j) ()) hg
              jLeqi = Map.lookup (Edge (NodeRigid j) (NodeRigid i) ()) hg
          case (iLeqj, jLeqi) of
            (Nothing, Nothing) -> Nothing -- maximum as size expression
            (Just l, Nothing) | Offset k <- toWeight l ->
              if k + n <= m then Just a1
              else Nothing -- no guaranteed infimum
            (Nothing, Just l) | Offset k <- toWeight l ->
              if k + m <= n then Just a2
              else Nothing
            (Just{}, Just{}) -> Nothing
    {-
          let lbi = incoming hg (NodeRigid i)
              lbj = incoming hg (NodeRigid j)
              srci = Set.fromList $ map src lbi
              srcj = Set.fromList $ map src lbj
              srcs =  Set.intersection srci srcj
    -}
        _ -> trace ("cannot compute glb of " ++ prettyShow a1 ++ " and " ++ prettyShow a2) $
          Nothing -- TODO!
    -}

    findRigidBelow :: (Ord r, Ord f) => HypGraph r f -> (SizeExpr' r f) -> Maybe (SizeExpr' r f)
    findRigidBelow :: forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    findRigidBelow HypGraph r f
    hg (Rigid r
    i Offset
    m) | Offset
    m Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    < Offset
    0 = do
      let v :: Node r f
    v     = r -> Node r f
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid r
    i
          preds :: [Edge' r f Label]
    preds = HypGraph r f -> Node r f -> [Edge' r f Label]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> Node r f -> [Edge' r f a]
    incoming HypGraph r f
    hg Node r f
    v
          filt :: Edge' r f Label -> Maybe (Node r f, Offset)
    filt e :: Edge' r f Label
    e@(Edge Node r f
    n Node r f
    n' Label
    l)
            | Node r f
    n' Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    == Node r f
    v   =
              case Label -> Weight
    toWeight Label
    l of
                Weight
    Infinity -> Maybe (Node r f, Offset)
    forall a. Maybe a
    Nothing
                Offset Offset
    o -> if Offset
    o Offset -> Offset -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Offset
    m then (Node r f, Offset) -> Maybe (Node r f, Offset)
    forall a. a -> Maybe a
    Just (Node r f
    n, Offset
    o) else Maybe (Node r f, Offset)
    forall a. Maybe a
    Nothing
            | Bool
    otherwise = Maybe (Node r f, Offset)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
                -- error $ "findRigidBelow: impossible: " ++ prettyShow e
          cands :: [(Node r f, Offset)]
    cands = (Edge' r f Label -> Maybe (Node r f, Offset))
    -> [Edge' r f Label] -> [(Node r f, Offset)]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe Edge' r f Label -> Maybe (Node r f, Offset)
    filt [Edge' r f Label]
    preds
      (n, o) <- do
        case [(Node r f, Offset)]
    cands of
          []  -> Maybe (Node r f, Offset)
    forall a. Maybe a
    Nothing
          [(Node r f, Offset)
    c] -> (Node r f, Offset) -> Maybe (Node r f, Offset)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Node r f, Offset)
    c
          [(Node r f, Offset)]
    _   -> (Node r f, Offset) -> Maybe (Node r f, Offset)
    forall a. a -> Maybe a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ((Node r f, Offset) -> Maybe (Node r f, Offset))
    -> (Node r f, Offset) -> Maybe (Node r f, Offset)
    forall a b. (a -> b) -> a -> b
    $
                   ((Node r f, Offset) -> (Node r f, Offset) -> Ordering)
    -> [(Node r f, Offset)] -> (Node r f, Offset)
    forall (t :: * -> *) a.
    Foldable t =>
    (a -> a -> Ordering) -> t a -> a
    List.maximumBy (Offset -> Offset -> Ordering
    forall a. Ord a => a -> a -> Ordering
    compare (Offset -> Offset -> Ordering)
    -> ((Node r f, Offset) -> Offset)
    -> (Node r f, Offset)
    -> (Node r f, Offset)
    -> Ordering
    forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
    `on` (Node r f, Offset) -> Offset
    forall a b. (a, b) -> b
    snd) ([(Node r f, Offset)] -> (Node r f, Offset))
    -> [(Node r f, Offset)] -> (Node r f, Offset)
    forall a b. (a -> b) -> a -> b
    $
                     ((Node r f, Offset) -> Bool)
    -> [(Node r f, Offset)] -> [(Node r f, Offset)]
    forall a. (a -> Bool) -> [a] -> [a]
    filter ((Node r f
    forall rigid flex. Node rigid flex
    NodeZero Node r f -> Node r f -> Bool
    forall a. Eq a => a -> a -> Bool
    /=) (Node r f -> Bool)
    -> ((Node r f, Offset) -> Node r f) -> (Node r f, Offset) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Node r f, Offset) -> Node r f
    forall a b. (a, b) -> a
    fst) [(Node r f, Offset)]
    cands
      let offset = Offset
    m Offset -> Offset -> Offset
    forall a. Num a => a -> a -> a
    - Offset
    o
      unless (offset >= 0) __IMPOSSIBLE__
      return $ nodeToSizeExpr n `plus` offset
    findRigidBelow HypGraph r f
    hg SizeExpr' r f
    e = Maybe (SizeExpr' r f)
    forall a. HasCallStack => a
    __IMPOSSIBLE__
      -- error $ "findRigidBelow: impossible: " ++ prettyShow e

    solveGraph
      :: forall r f. (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
      => Polarities f
      -> HypGraph r f
      -> ConGraph r f
      -> Either Error (Solution r f)
    solveGraph :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
    Polarities f
    -> HypGraph r f
    -> HypGraph r f
    -> Either (TCMT IO Doc) (Solution r f)
    solveGraph Polarities f
    pols HypGraph r f
    hg HypGraph r f
    g = do
      let (Bounds Bound r f
    lbs Bound r f
    ubs Set f
    fs) = HypGraph r f -> Bounds r f
    forall r f. (Ord r, Ord f) => ConGraph r f -> Bounds r f
    bounds HypGraph r f
    g
          -- flexibles to solve for
          xs :: [f]
          xs :: [f]
    xs = Set f -> [f]
    forall a. Set a -> [a]
    Set.toAscList (Set f -> [f]) -> Set f -> [f]
    forall a b. (a -> b) -> a -> b
    $ [Set f] -> Set f
    forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
    Set.unions [ Bound r f -> Set f
    forall k a. Map k a -> Set k
    Map.keysSet Bound r f
    lbs, Bound r f -> Set f
    forall k a. Map k a -> Set k
    Map.keysSet Bound r f
    ubs, Set f
    fs ]
      -- iterate over all flexible variables
      xas <- [Maybe (f, SizeExpr' r f)] -> [(f, SizeExpr' r f)]
    forall a. [Maybe a] -> [a]
    catMaybes ([Maybe (f, SizeExpr' r f)] -> [(f, SizeExpr' r f)])
    -> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)]
    -> Either (TCMT IO Doc) [(f, SizeExpr' r f)]
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
        [f]
    -> (f -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
    -> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    t a -> (a -> m b) -> m (t b)
    forM [f]
    xs ((f -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
     -> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)])
    -> (f -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f)))
    -> Either (TCMT IO Doc) [Maybe (f, SizeExpr' r f)]
    forall a b. (a -> b) -> a -> b
    $ \ f
    x -> (SizeExpr' r f -> (f, SizeExpr' r f))
    -> Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f)
    forall a b. (a -> b) -> Maybe a -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap (f
    x,) (Maybe (SizeExpr' r f) -> Maybe (f, SizeExpr' r f))
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    -> Either (TCMT IO Doc) (Maybe (f, SizeExpr' r f))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> do
          -- get lower and upper bounds for flexible x
          let lx :: [SizeExpr' r f]
    lx = Set (SizeExpr' r f) -> [SizeExpr' r f]
    forall a. Set a -> [a]
    Set.toList (Set (SizeExpr' r f) -> [SizeExpr' r f])
    -> Set (SizeExpr' r f) -> [SizeExpr' r f]
    forall a b. (a -> b) -> a -> b
    $ Set (SizeExpr' r f) -> f -> Bound r f -> Set (SizeExpr' r f)
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Set (SizeExpr' r f)
    forall a. Set a
    Set.empty f
    x Bound r f
    lbs
              ux :: [SizeExpr' r f]
    ux = Set (SizeExpr' r f) -> [SizeExpr' r f]
    forall a. Set a -> [a]
    Set.toList (Set (SizeExpr' r f) -> [SizeExpr' r f])
    -> Set (SizeExpr' r f) -> [SizeExpr' r f]
    forall a b. (a -> b) -> a -> b
    $ Set (SizeExpr' r f) -> f -> Bound r f -> Set (SizeExpr' r f)
    forall k a. Ord k => a -> k -> Map k a -> a
    Map.findWithDefault Set (SizeExpr' r f)
    forall a. Set a
    Set.empty f
    x Bound r f
    ubs
          String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "lower bounds for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ f -> String
    forall a. Pretty a => a -> String
    prettyShow f
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [SizeExpr' r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [SizeExpr' r f]
    lx)
          String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "upper bounds for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ f -> String
    forall a. Pretty a => a -> String
    prettyShow f
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ [SizeExpr' r f] -> String
    forall a. Pretty a => a -> String
    prettyShow [SizeExpr' r f]
    ux)
          -- compute maximum of lower bounds
          lb <- do
            case [SizeExpr' r f]
    lx of
              []     -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ Maybe (SizeExpr' r f)
    forall a. Maybe a
    Nothing
              (SizeExpr' r f
    a:[SizeExpr' r f]
    as) -> do
                case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    lub HypGraph r f
    hg) SizeExpr' r f
    a [SizeExpr' r f]
    as of
                  Just SizeExpr' r f
    l  -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just (SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> SizeExpr' r f
    forall a. TruncateOffset a => a -> a
    truncateOffset SizeExpr' r f
    l
                  Maybe (SizeExpr' r f)
    Nothing -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. a -> Either a b
    Left (TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $
                    TCMT IO Doc
    "inconsistent lower bound for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> f -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => f -> m Doc
    P.prettyTCM f
    x
          -- compute minimum of upper bounds
          ub <- do
            case ux of
              []     -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ Maybe (SizeExpr' r f)
    forall a. Maybe a
    Nothing
              (SizeExpr' r f
    a:[SizeExpr' r f]
    as) -> do
                case (SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f))
    -> SizeExpr' r f -> [SizeExpr' r f] -> Maybe (SizeExpr' r f)
    forall (t :: * -> *) (m :: * -> *) b a.
    (Foldable t, Monad m) =>
    (b -> a -> m b) -> b -> t a -> m b
    foldM (HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    glb HypGraph r f
    hg) SizeExpr' r f
    a [SizeExpr' r f]
    as of
                  Just SizeExpr' r f
    l | SizeExpr' r f -> Bool
    forall a. ValidOffset a => a -> Bool
    validOffset SizeExpr' r f
    l                  -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    l
                         | Just SizeExpr' r f
    l' <- HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall r f.
    (Ord r, Ord f) =>
    HypGraph r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    findRigidBelow HypGraph r f
    hg SizeExpr' r f
    l -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    l'
                  Maybe (SizeExpr' r f)
    _ -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. a -> Either a b
    Left (TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> TCMT IO Doc -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $
                    TCMT IO Doc
    "inconsistent upper bound for" TCMT IO Doc -> TCMT IO Doc -> TCMT IO Doc
    forall (m :: * -> *). Applicative m => m Doc -> m Doc -> m Doc
    P.<+> f -> TCMT IO Doc
    forall a (m :: * -> *). (PrettyTCM a, MonadPretty m) => a -> m Doc
    forall (m :: * -> *). MonadPretty m => f -> m Doc
    P.prettyTCM f
    x
          case (lb, ub) of
            (Just SizeExpr' r f
    l, Maybe (SizeExpr' r f)
    Nothing) -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    l  -- solve x = lower bound
            (Maybe (SizeExpr' r f)
    Nothing, Just SizeExpr' r f
    u) -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    u  -- solve x = upper bound
            (Just SizeExpr' r f
    l,  Just SizeExpr' r f
    u) -> do
              String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "lower bound for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ f -> String
    forall a. Pretty a => a -> String
    prettyShow f
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    l)
              String -> Either (TCMT IO Doc) ()
    forall (f :: * -> *). Applicative f => String -> f ()
    traceM (String
    "upper bound for " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ f -> String
    forall a. Pretty a => a -> String
    prettyShow f
    x String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ String
    ": " String -> ShowS
    forall a. [a] -> [a] -> [a]
    ++ SizeExpr' r f -> String
    forall a. Pretty a => a -> String
    prettyShow SizeExpr' r f
    u)
              case Polarities f -> f -> Polarity
    forall flex. Ord flex => Polarities flex -> flex -> Polarity
    getPolarity Polarities f
    pols f
    x of
                Polarity
    Least    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    l
                Polarity
    Greatest -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return (Maybe (SizeExpr' r f)
     -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f)))
    -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a b. (a -> b) -> a -> b
    $ SizeExpr' r f -> Maybe (SizeExpr' r f)
    forall a. a -> Maybe a
    Just SizeExpr' r f
    u
            (Maybe (SizeExpr' r f), Maybe (SizeExpr' r f))
    _ -> Maybe (SizeExpr' r f)
    -> Either (TCMT IO Doc) (Maybe (SizeExpr' r f))
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return Maybe (SizeExpr' r f)
    forall a. Maybe a
    Nothing
      return $ Solution $ Map.fromDistinctAscList xas

    -- | Solve a forest of constraint graphs relative to a hypotheses graph.
    --   Concatenate individual solutions.
    solveGraphs
      :: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
      => Polarities f
      -> HypGraph r f
      -> ConGraphs r f
      -> Either Error (Solution r f)
    solveGraphs :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
    Polarities f
    -> HypGraph r f
    -> ConGraphs r f
    -> Either (TCMT IO Doc) (Solution r f)
    solveGraphs Polarities f
    pols HypGraph r f
    hg ConGraphs r f
    gs =
      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)
    -> ([Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f))
    -> [Map f (SizeExpr' r f)]
    -> Solution r f
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . [Map f (SizeExpr' r f)] -> Map f (SizeExpr' r f)
    forall (f :: * -> *) k a.
    (Foldable f, Ord k) =>
    f (Map k a) -> Map k a
    Map.unions ([Map f (SizeExpr' r f)] -> Solution r f)
    -> Either (TCMT IO Doc) [Map f (SizeExpr' r f)]
    -> Either (TCMT IO Doc) (Solution r f)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (HypGraph r f -> Either (TCMT IO Doc) (Map f (SizeExpr' r f)))
    -> ConGraphs r f -> Either (TCMT IO Doc) [Map f (SizeExpr' r f)]
    forall (t :: * -> *) (m :: * -> *) a b.
    (Traversable t, Monad m) =>
    (a -> m b) -> t a -> m (t b)
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
    mapM (Solution r f -> Map f (SizeExpr' r f)
    forall rigid flex.
    Solution rigid flex -> Map flex (SizeExpr' rigid flex)
    theSolution (Solution r f -> Map f (SizeExpr' r f))
    -> (HypGraph r f -> Either (TCMT IO Doc) (Solution r f))
    -> HypGraph r f
    -> Either (TCMT IO Doc) (Map f (SizeExpr' r f))
    forall (m :: * -> *) b c a.
    Functor m =>
    (b -> c) -> (a -> m b) -> a -> m c
    <.> Polarities f
    -> HypGraph r f
    -> HypGraph r f
    -> Either (TCMT IO Doc) (Solution r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
    Polarities f
    -> HypGraph r f
    -> HypGraph r f
    -> Either (TCMT IO Doc) (Solution r f)
    solveGraph Polarities f
    pols HypGraph r f
    hg) ConGraphs r f
    gs

    -- * Verify solution

    -- | Check that after substitution of the solution,
    --   constraints are implied by hypotheses.
    verifySolution
      :: (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f)
      => HypGraph r f
      -> [Constraint' r f]
      -> Solution r f
      -> Either Error ()
    verifySolution :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> [Constraint' r f] -> Solution r f -> Either (TCMT IO Doc) ()
    verifySolution HypGraph r f
    hg [Constraint' r f]
    cs Solution r f
    sol = do
      cs <- [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return ([Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f])
    -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall a b. (a -> b) -> a -> b
    $ Solution r f -> [Constraint' r f] -> [Constraint' r f]
    forall r f a. Substitute r f a => Solution r f -> a -> a
    subst Solution r f
    sol [Constraint' r f]
    cs
      traceM $ "substituted constraints " ++ prettyShow cs
      cs <- -- maybe (Left "solution produces inconsistency") Right $
              concat <$> mapM (simplify1 $ \ Constraint' r f
    c -> [Constraint' r f] -> Either (TCMT IO Doc) [Constraint' r f]
    forall a. a -> Either (TCMT IO Doc) a
    forall (m :: * -> *) a. Monad m => a -> m a
    return [Constraint' r f
    c]) cs
      traceM $ "simplified substituted constraints " ++ prettyShow cs
      -- cs <- maybe (Left "solution produces inconsistency") Right $
      --         simplifyWithHypotheses hg cs
      let g = [Constraint' r f] -> HypGraph r f
    forall rigid flex.
    (Ord rigid, Ord flex) =>
    [Constraint' rigid flex] -> Graph rigid flex Label
    graphFromConstraints [Constraint' r f]
    cs
      unless (hg `implies` g) $
        Left "solution not implied by hypotheses"
    {-
      case simplifyWithHypotheses hg $ subst sol cs of
        Nothing -> Left "solution produces inconsistency"
        Just [] -> Right ()
        Just cs -> Left $ "solution leaves constraints " ++ prettyShow cs
    -}

    -- | Iterate solver until no more metas can be solved.
    --
    --   This might trigger a (wanted) error on the second iteration (see Issue 2096)
    --   which would otherwise go unnoticed.

    iterateSolver
      :: (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f)
      => Polarities f
         -- ^ Meta variable polarities (prefer lower or upper solution?).
      -> HypGraph r f
         -- ^ Hypotheses (assumed to have no metas, so, fixed during iteration).
      -> [Constraint' r f]
         -- ^ Constraints to solve.
      -> Solution r f
         -- ^ Previous substitution (already applied to constraints).
      -> Either Error (Solution r f)
         -- ^ Accumulated substition.

    iterateSolver :: forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, PrettyTCM f, Show r, Show f) =>
    Polarities f
    -> HypGraph r f
    -> [Constraint' r f]
    -> Solution r f
    -> Either (TCMT IO Doc) (Solution r f)
    iterateSolver Polarities f
    pols HypGraph r f
    hg [Constraint' r f]
    cs Solution r f
    sol0 = do
      g <- [Constraint' r f]
    -> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f) =>
    [Constraint' r f]
    -> HypGraph r f -> Either (TCMT IO Doc) (HypGraph r f)
    constraintGraph [Constraint' r f]
    cs HypGraph r f
    hg
      sol <- solveGraph pols hg g
      traceM $ "(partial) solution " ++ prettyShow sol
      if null sol then return sol0 else
        iterateSolver pols hg (subst sol cs) $ Solution $
          Map.unionWith __IMPOSSIBLE__ (theSolution sol) $
            theSolution $ subst sol sol0

    -- * Tests

    testSuccs :: Ord f => Map (Node [Char] f) [Edge' [Char] f Label]
    testSuccs :: forall f. Ord f => Map (Node String f) [Edge' String f Label]
    testSuccs = Graph String f Label
    -> [Node String f] -> Map (Node String f) [Edge' String f Label]
    forall r f a.
    (Ord r, Ord f) =>
    Graph r f a -> [Node r f] -> Map (Node r f) [Edge' r f a]
    commonSuccs Graph String f Label
    hg [Node String f
    forall {flex}. Node String flex
    n1,Node String f
    forall {flex}. Node String flex
    n2]
      where
        n1 :: Node String flex
    n1 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "i"
        n2 :: Node String flex
    n2 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "j"
        n3 :: Node String flex
    n3 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "k"
        n4 :: Node String flex
    n4 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "l"
        n5 :: Node String flex
    n5 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "m"
        hg :: Graph String f Label
    hg = [Edge' String f Label] -> Graph String f Label
    forall n e. Ord n => [Edge n e] -> Graph n e
    Graph.fromEdges
             [ Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    1
             , Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    2
             , Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    3
             , Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n3 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    4
             , Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n4 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    5
             , Node String f -> Node String f -> Label -> Edge' String f Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n5 (Label -> Edge' String f Label) -> Label -> Edge' String f Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    6
             ]

    -- testLub = smallest hg $ Map.keys $ commonSuccs hg [n1,n2] --
    testLub :: (Pretty f, Ord f, Show f) => Maybe (SizeExpr' [Char] f)
    testLub :: forall f. (Pretty f, Ord f, Show f) => Maybe (SizeExpr' String f)
    testLub = HypGraph String f
    -> SizeExpr' String f
    -> SizeExpr' String f
    -> Maybe (SizeExpr' String f)
    forall r f.
    (Ord r, Ord f, Pretty r, Pretty f, Show r, Show f) =>
    HypGraph r f
    -> SizeExpr' r f -> SizeExpr' r f -> Maybe (SizeExpr' r f)
    lub HypGraph String f
    hg (String -> Offset -> SizeExpr' String f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid String
    "i" Offset
    0) (String -> Offset -> SizeExpr' String f
    forall rigid flex. rigid -> Offset -> SizeExpr' rigid flex
    Rigid String
    "j" Offset
    2)
      where
        n1 :: Node String flex
    n1 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "i"
        n2 :: Node String flex
    n2 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "j"
        n3 :: Node String flex
    n3 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "k"
        n4 :: Node String flex
    n4 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "l"
        n5 :: Node String flex
    n5 = String -> Node String flex
    forall rigid flex. rigid -> Node rigid flex
    NodeRigid String
    "m"
        hg :: HypGraph String f
    hg = [Edge (Node String f) Label] -> HypGraph String f
    forall n e. Ord n => [Edge n e] -> Graph n e
    Graph.fromEdges
             [ Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n3 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n4 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    2
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n1 Node String f
    forall {flex}. Node String flex
    n5 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    4
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n3 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    1
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n4 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    3
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n2 Node String f
    forall {flex}. Node String flex
    n5 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    5
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n3 Node String f
    forall {flex}. Node String flex
    n4 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Le Offset
    0
             , Node String f
    -> Node String f -> Label -> Edge (Node String f) Label
    forall n e. n -> n -> e -> Edge n e
    Graph.Edge Node String f
    forall {flex}. Node String flex
    n3 Node String f
    forall {flex}. Node String flex
    n5 (Label -> Edge (Node String f) Label)
    -> Label -> Edge (Node String f) Label
    forall a b. (a -> b) -> a -> b
    $ Cmp -> Offset -> Label
    Label Cmp
    Lt Offset
    0
             ]