    -- | Implementation of unification and other core type system building
    -- blocks.
    module Language.Futhark.TypeChecker.Unify
      ( Constraint (..),
        Usage (..),
        mkUsage,
        mkUsage',
        Level,
        Constraints,
        MonadUnify (..),
        Rigidity (..),
        RigidSource (..),
        BreadCrumbs,
        sizeFree,
        noBreadCrumbs,
        hasNoBreadCrumbs,
        dimNotes,
        zeroOrderType,
        arrayElemType,
        mustHaveConstr,
        mustHaveField,
        mustBeOneOf,
        equalityType,
        normType,
        normTypeFully,
        unify,
        unifyMostCommon,
        doUnification,
      )
    where

    import Control.Monad
    import Control.Monad.Except
    import Control.Monad.Identity
    import Control.Monad.Reader
    import Control.Monad.State
    import Data.List qualified as L
    import Data.Map.Strict qualified as M
    import Data.Maybe
    import Data.Set qualified as S
    import Data.Text qualified as T
    import Futhark.Util (topologicalSort)
    import Futhark.Util.Pretty
    import Language.Futhark
    import Language.Futhark.Traversals
    import Language.Futhark.TypeChecker.Monad hiding (BoundV)
    import Language.Futhark.TypeChecker.Types

    -- | A piece of information that describes what process the type
    -- checker currently performing.  This is used to give better error
    -- messages for unification errors.
    data BreadCrumb
      = MatchingTypes StructType StructType
      | MatchingFields [Name]
      | MatchingConstructor Name
      | Matching (Doc ())

    instance Pretty BreadCrumb where
      pretty :: forall ann. BreadCrumb -> Doc ann
    pretty (MatchingTypes StructType
    t1 StructType
    t2) =
        Doc ann
    "When matching type"
          Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc ann -> Doc ann
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t1)
          Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ann
    "with"
          Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc ann -> Doc ann
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t2)
      pretty (MatchingFields [Name]
    fields) =
        Doc ann
    "When matching types of record field"
          Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    dquotes ([Doc ann] -> Doc ann
    forall a. Monoid a => [a] -> a
    mconcat ([Doc ann] -> Doc ann) -> [Doc ann] -> Doc ann
    forall a b. (a -> b) -> a -> b
    $ Doc ann -> [Doc ann] -> [Doc ann]
    forall ann. Doc ann -> [Doc ann] -> [Doc ann]
    punctuate Doc ann
    "." ([Doc ann] -> [Doc ann]) -> [Doc ann] -> [Doc ann]
    forall a b. (a -> b) -> a -> b
    $ (Name -> Doc ann) -> [Name] -> [Doc ann]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty [Name]
    fields)
          Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> Doc ann
    forall ann. Doc ann
    dot
      pretty (MatchingConstructor Name
    c) =
        Doc ann
    "When matching types of constructor" Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty Name
    c) Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> Doc ann
    forall ann. Doc ann
    dot
      pretty (Matching Doc ()
    s) =
        Doc () -> Doc ann
    forall ann xxx. Doc ann -> Doc xxx
    unAnnotate Doc ()
    s

    -- | Unification failures can occur deep down inside complicated types
    -- (consider nested records).  We leave breadcrumbs behind us so we
    -- can report the path we took to find the mismatch.
    newtype BreadCrumbs = BreadCrumbs [BreadCrumb]

    -- | An empty path.
    noBreadCrumbs :: BreadCrumbs
    noBreadCrumbs :: BreadCrumbs
    noBreadCrumbs = [BreadCrumb] -> BreadCrumbs
    BreadCrumbs []

    -- | Is the path empty?
    hasNoBreadCrumbs :: BreadCrumbs -> Bool
    hasNoBreadCrumbs :: BreadCrumbs -> Bool
    hasNoBreadCrumbs (BreadCrumbs [BreadCrumb]
    xs) = [BreadCrumb] -> Bool
    forall a. [a] -> Bool
    forall (t :: * -> *) a. Foldable t => t a -> Bool
    null [BreadCrumb]
    xs

    -- | Drop a breadcrumb on the path behind you.
    breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb (MatchingFields [Name]
    xs) (BreadCrumbs (MatchingFields [Name]
    ys : [BreadCrumb]
    bcs)) =
      [BreadCrumb] -> BreadCrumbs
    BreadCrumbs ([BreadCrumb] -> BreadCrumbs) -> [BreadCrumb] -> BreadCrumbs
    forall a b. (a -> b) -> a -> b
    $ [Name] -> BreadCrumb
    MatchingFields ([Name]
    ys [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ [Name]
    xs) BreadCrumb -> [BreadCrumb] -> [BreadCrumb]
    forall a. a -> [a] -> [a]
    : [BreadCrumb]
    bcs
    breadCrumb BreadCrumb
    bc (BreadCrumbs [BreadCrumb]
    bcs) =
      [BreadCrumb] -> BreadCrumbs
    BreadCrumbs ([BreadCrumb] -> BreadCrumbs) -> [BreadCrumb] -> BreadCrumbs
    forall a b. (a -> b) -> a -> b
    $ BreadCrumb
    bc BreadCrumb -> [BreadCrumb] -> [BreadCrumb]
    forall a. a -> [a] -> [a]
    : [BreadCrumb]
    bcs

    instance Pretty BreadCrumbs where
      pretty :: forall ann. BreadCrumbs -> Doc ann
    pretty (BreadCrumbs []) = Doc ann
    forall a. Monoid a => a
    mempty
      pretty (BreadCrumbs [BreadCrumb]
    bcs) = Doc ann
    forall ann. Doc ann
    line Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> [Doc ann] -> Doc ann
    forall a. [Doc a] -> Doc a
    stack ((BreadCrumb -> Doc ann) -> [BreadCrumb] -> [Doc ann]
    forall a b. (a -> b) -> [a] -> [b]
    map BreadCrumb -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. BreadCrumb -> Doc ann
    pretty [BreadCrumb]
    bcs)

    -- | A usage that caused a type constraint.
    data Usage = Usage (Maybe T.Text) Loc
      deriving (Int -> Usage -> ShowS
    [Usage] -> ShowS
    Usage -> String
    (Int -> Usage -> ShowS)
    -> (Usage -> String) -> ([Usage] -> ShowS) -> Show Usage
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Usage -> ShowS
    showsPrec :: Int -> Usage -> ShowS
    $cshow :: Usage -> String
    show :: Usage -> String
    $cshowList :: [Usage] -> ShowS
    showList :: [Usage] -> ShowS
    Show)

    -- | Construct a 'Usage' from a location and a description.
    mkUsage :: (Located a) => a -> T.Text -> Usage
    mkUsage :: forall a. Located a => a -> Text -> Usage
    mkUsage = (Text -> Loc -> Usage) -> Loc -> Text -> Usage
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip (Maybe Text -> Loc -> Usage
    Usage (Maybe Text -> Loc -> Usage)
    -> (Text -> Maybe Text) -> Text -> Loc -> Usage
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Text -> Maybe Text
    forall a. a -> Maybe a
    Just) (Loc -> Text -> Usage) -> (a -> Loc) -> a -> Text -> Usage
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Loc
    forall a. Located a => a -> Loc
    locOf

    -- | Construct a 'Usage' that has just a location, but no particular
    -- description.
    mkUsage' :: (Located a) => a -> Usage
    mkUsage' :: forall a. Located a => a -> Usage
    mkUsage' = Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing (Loc -> Usage) -> (a -> Loc) -> a -> Usage
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . a -> Loc
    forall a. Located a => a -> Loc
    locOf

    instance Pretty Usage where
      pretty :: forall ann. Usage -> Doc ann
    pretty (Usage Maybe Text
    Nothing Loc
    loc) = Doc ann
    "use at " Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> Text -> Doc ann
    forall a. Text -> Doc a
    textwrap (Loc -> Text
    forall a. Located a => a -> Text
    locText Loc
    loc)
      pretty (Usage (Just Text
    s) Loc
    loc) = Text -> Doc ann
    forall a. Text -> Doc a
    textwrap Text
    s Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ann
    "at" Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Text -> Doc ann
    forall a. Text -> Doc a
    textwrap (Loc -> Text
    forall a. Located a => a -> Text
    locText Loc
    loc)

    instance Located Usage where
      locOf :: Usage -> Loc
    locOf (Usage Maybe Text
    _ Loc
    loc) = Loc -> Loc
    forall a. Located a => a -> Loc
    locOf Loc
    loc

    -- | The level at which a type variable is bound.  Higher means
    -- deeper.  We can only unify a type variable at level @i@ with a type
    -- @t@ if all type names that occur in @t@ are at most at level @i@.
    type Level = Int

    -- | A constraint on a yet-ambiguous type variable.
    data Constraint
      = NoConstraint Liftedness Usage
      | ParamType Liftedness Loc
      | Constraint StructRetType Usage
      | Overloaded [PrimType] Usage
      | HasFields Liftedness (M.Map Name StructType) Usage
      | Equality Usage
      | HasConstrs Liftedness (M.Map Name [StructType]) Usage
      | ParamSize Loc
      | -- | Is not actually a type, but a term-level size,
        -- possibly already set to something specific.
        Size (Maybe Exp) Usage
      | -- | A size that does not unify with anything -
        -- created from the result of applying a function
        -- whose return size is existential, or otherwise
        -- hiding a size.
        UnknownSize Loc RigidSource
      deriving (Int -> Constraint -> ShowS
    [Constraint] -> ShowS
    Constraint -> String
    (Int -> Constraint -> ShowS)
    -> (Constraint -> String)
    -> ([Constraint] -> ShowS)
    -> Show Constraint
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Constraint -> ShowS
    showsPrec :: Int -> Constraint -> ShowS
    $cshow :: Constraint -> String
    show :: Constraint -> String
    $cshowList :: [Constraint] -> ShowS
    showList :: [Constraint] -> ShowS
    Show)

    instance Located Constraint where
      locOf :: Constraint -> Loc
    locOf (NoConstraint Liftedness
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (ParamType Liftedness
    _ Loc
    usage) = Loc -> Loc
    forall a. Located a => a -> Loc
    locOf Loc
    usage
      locOf (Constraint StructRetType
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (Overloaded [PrimType]
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (HasFields Liftedness
    _ Map Name StructType
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (Equality Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (HasConstrs Liftedness
    _ Map Name [StructType]
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (ParamSize Loc
    loc) = Loc -> Loc
    forall a. Located a => a -> Loc
    locOf Loc
    loc
      locOf (Size Maybe Exp
    _ Usage
    usage) = Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage
      locOf (UnknownSize Loc
    loc RigidSource
    _) = Loc -> Loc
    forall a. Located a => a -> Loc
    locOf Loc
    loc

    -- | Mapping from fresh type variables, instantiated from the type
    -- schemes of polymorphic functions, to (possibly) specific types as
    -- determined on application and the location of that application, or
    -- a partial constraint on their type.
    type Constraints = M.Map VName (Level, Constraint)

    lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
    lookupSubst :: VName -> Constraints -> Maybe (Subst StructRetType)
    lookupSubst VName
    v Constraints
    constraints = case (Int, Constraint) -> Constraint
    forall a b. (a, b) -> b
    snd ((Int, Constraint) -> Constraint)
    -> Maybe (Int, Constraint) -> Maybe Constraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints of
      Just (Constraint StructRetType
    t Usage
    _) -> Subst StructRetType -> Maybe (Subst StructRetType)
    forall a. a -> Maybe a
    Just (Subst StructRetType -> Maybe (Subst StructRetType))
    -> Subst StructRetType -> Maybe (Subst StructRetType)
    forall a b. (a -> b) -> a -> b
    $ [TypeParam] -> StructRetType -> Subst StructRetType
    forall t. [TypeParam] -> t -> Subst t
    Subst [] (StructRetType -> Subst StructRetType)
    -> StructRetType -> Subst StructRetType
    forall a b. (a -> b) -> a -> b
    $ TypeSubs -> StructRetType -> StructRetType
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
    `lookupSubst` Constraints
    constraints) StructRetType
    t
      Just (Size (Just Exp
    d) Usage
    _) ->
        Subst StructRetType -> Maybe (Subst StructRetType)
    forall a. a -> Maybe a
    Just (Subst StructRetType -> Maybe (Subst StructRetType))
    -> Subst StructRetType -> Maybe (Subst StructRetType)
    forall a b. (a -> b) -> a -> b
    $ Exp -> Subst StructRetType
    forall t. Exp -> Subst t
    ExpSubst (Exp -> Subst StructRetType) -> Exp -> Subst StructRetType
    forall a b. (a -> b) -> a -> b
    $ TypeSubs -> Exp -> Exp
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
    `lookupSubst` Constraints
    constraints) Exp
    d
      Maybe Constraint
    _ -> Maybe (Subst StructRetType)
    forall a. Maybe a
    Nothing

    -- | The source of a rigid size.
    data RigidSource
      = -- | A function argument that is not a constant or variable name.
        RigidArg (Maybe (QualName VName)) T.Text
      | -- | An existential return size.
        RigidRet (Maybe (QualName VName))
      | -- | Similarly to 'RigidRet', but produce by a loop.
        RigidLoop
      | -- | Produced by a complicated slice expression.
        RigidSlice (Maybe Size) T.Text
      | -- | Produced by a complicated range expression.
        RigidRange
      | -- | Mismatch in branches.
        RigidCond StructType StructType
      | -- | Invented during unification.
        RigidUnify
      | -- | A name used in a size went out of scope.
        RigidOutOfScope Loc VName
      deriving (RigidSource -> RigidSource -> Bool
    (RigidSource -> RigidSource -> Bool)
    -> (RigidSource -> RigidSource -> Bool) -> Eq RigidSource
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: RigidSource -> RigidSource -> Bool
    == :: RigidSource -> RigidSource -> Bool
    $c/= :: RigidSource -> RigidSource -> Bool
    /= :: RigidSource -> RigidSource -> Bool
    Eq, Eq RigidSource
    Eq RigidSource =>
    (RigidSource -> RigidSource -> Ordering)
    -> (RigidSource -> RigidSource -> Bool)
    -> (RigidSource -> RigidSource -> Bool)
    -> (RigidSource -> RigidSource -> Bool)
    -> (RigidSource -> RigidSource -> Bool)
    -> (RigidSource -> RigidSource -> RigidSource)
    -> (RigidSource -> RigidSource -> RigidSource)
    -> Ord RigidSource
    RigidSource -> RigidSource -> Bool
    RigidSource -> RigidSource -> Ordering
    RigidSource -> RigidSource -> RigidSource
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: RigidSource -> RigidSource -> Ordering
    compare :: RigidSource -> RigidSource -> Ordering
    $c< :: RigidSource -> RigidSource -> Bool
    < :: RigidSource -> RigidSource -> Bool
    $c<= :: RigidSource -> RigidSource -> Bool
    <= :: RigidSource -> RigidSource -> Bool
    $c> :: RigidSource -> RigidSource -> Bool
    > :: RigidSource -> RigidSource -> Bool
    $c>= :: RigidSource -> RigidSource -> Bool
    >= :: RigidSource -> RigidSource -> Bool
    $cmax :: RigidSource -> RigidSource -> RigidSource
    max :: RigidSource -> RigidSource -> RigidSource
    $cmin :: RigidSource -> RigidSource -> RigidSource
    min :: RigidSource -> RigidSource -> RigidSource
    Ord, Int -> RigidSource -> ShowS
    [RigidSource] -> ShowS
    RigidSource -> String
    (Int -> RigidSource -> ShowS)
    -> (RigidSource -> String)
    -> ([RigidSource] -> ShowS)
    -> Show RigidSource
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> RigidSource -> ShowS
    showsPrec :: Int -> RigidSource -> ShowS
    $cshow :: RigidSource -> String
    show :: RigidSource -> String
    $cshowList :: [RigidSource] -> ShowS
    showList :: [RigidSource] -> ShowS
    Show)

    -- | The ridigity of a size variable.  All rigid sizes are tagged with
    -- information about how they were generated.
    data Rigidity = Rigid RigidSource | Nonrigid
      deriving (Rigidity -> Rigidity -> Bool
    (Rigidity -> Rigidity -> Bool)
    -> (Rigidity -> Rigidity -> Bool) -> Eq Rigidity
    forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
    $c== :: Rigidity -> Rigidity -> Bool
    == :: Rigidity -> Rigidity -> Bool
    $c/= :: Rigidity -> Rigidity -> Bool
    /= :: Rigidity -> Rigidity -> Bool
    Eq, Eq Rigidity
    Eq Rigidity =>
    (Rigidity -> Rigidity -> Ordering)
    -> (Rigidity -> Rigidity -> Bool)
    -> (Rigidity -> Rigidity -> Bool)
    -> (Rigidity -> Rigidity -> Bool)
    -> (Rigidity -> Rigidity -> Bool)
    -> (Rigidity -> Rigidity -> Rigidity)
    -> (Rigidity -> Rigidity -> Rigidity)
    -> Ord Rigidity
    Rigidity -> Rigidity -> Bool
    Rigidity -> Rigidity -> Ordering
    Rigidity -> Rigidity -> Rigidity
    forall a.
    Eq a =>
    (a -> a -> Ordering)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> Bool)
    -> (a -> a -> a)
    -> (a -> a -> a)
    -> Ord a
    $ccompare :: Rigidity -> Rigidity -> Ordering
    compare :: Rigidity -> Rigidity -> Ordering
    $c< :: Rigidity -> Rigidity -> Bool
    < :: Rigidity -> Rigidity -> Bool
    $c<= :: Rigidity -> Rigidity -> Bool
    <= :: Rigidity -> Rigidity -> Bool
    $c> :: Rigidity -> Rigidity -> Bool
    > :: Rigidity -> Rigidity -> Bool
    $c>= :: Rigidity -> Rigidity -> Bool
    >= :: Rigidity -> Rigidity -> Bool
    $cmax :: Rigidity -> Rigidity -> Rigidity
    max :: Rigidity -> Rigidity -> Rigidity
    $cmin :: Rigidity -> Rigidity -> Rigidity
    min :: Rigidity -> Rigidity -> Rigidity
    Ord, Int -> Rigidity -> ShowS
    [Rigidity] -> ShowS
    Rigidity -> String
    (Int -> Rigidity -> ShowS)
    -> (Rigidity -> String) -> ([Rigidity] -> ShowS) -> Show Rigidity
    forall a.
    (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
    $cshowsPrec :: Int -> Rigidity -> ShowS
    showsPrec :: Int -> Rigidity -> ShowS
    $cshow :: Rigidity -> String
    show :: Rigidity -> String
    $cshowList :: [Rigidity] -> ShowS
    showList :: [Rigidity] -> ShowS
    Show)

    prettySource :: Loc -> Loc -> RigidSource -> Doc ()
    prettySource :: Loc -> Loc -> RigidSource -> Doc ()
    prettySource Loc
    ctx Loc
    loc (RigidRet Maybe (QualName VName)
    Nothing) =
      Doc ()
    "is unknown size returned by function at"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
    prettySource Loc
    ctx Loc
    loc (RigidRet (Just QualName VName
    fname)) =
      Doc ()
    "is unknown size returned by"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (QualName VName -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. QualName VName -> Doc ann
    pretty QualName VName
    fname)
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "at"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
    prettySource Loc
    ctx Loc
    loc (RigidArg Maybe (QualName VName)
    fname Text
    arg) =
      Doc ()
    "is value of argument"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (Doc Any -> Doc ()
    forall ann xxx. Doc ann -> Doc xxx
    shorten (Text -> Doc Any
    forall a. Text -> Doc a
    forall a ann. Pretty a => a -> Doc ann
    pretty Text
    arg))
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "passed to"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    forall ann. Doc ann
    fname'
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "at"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
      where
        fname' :: Doc ann
    fname' = Doc ann
    -> (QualName VName -> Doc ann) -> Maybe (QualName VName) -> Doc ann
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Doc ann
    "function" (Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    dquotes (Doc ann -> Doc ann)
    -> (QualName VName -> Doc ann) -> QualName VName -> Doc ann
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . QualName VName -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. QualName VName -> Doc ann
    pretty) Maybe (QualName VName)
    fname
    prettySource Loc
    ctx Loc
    loc (RigidSlice Maybe Exp
    d Text
    slice) =
      Doc ()
    "is size produced by slice"
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (Doc Any -> Doc ()
    forall ann xxx. Doc ann -> Doc xxx
    shorten (Text -> Doc Any
    forall a. Text -> Doc a
    forall a ann. Pretty a => a -> Doc ann
    pretty Text
    slice))
        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    forall ann. Doc ann
    d_desc
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "at"
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
      where
        d_desc :: Doc ann
    d_desc = case Maybe Exp
    d of
          Just Exp
    d' -> Doc ann
    "of dimension of size " Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> Doc ann -> Doc ann
    forall ann. Doc ann -> Doc ann
    dquotes (Exp -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Exp -> Doc ann
    pretty Exp
    d') Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> Doc ann
    " "
          Maybe Exp
    Nothing -> Doc ann
    forall a. Monoid a => a
    mempty
    prettySource Loc
    ctx Loc
    loc RigidSource
    RigidLoop =
      Doc ()
    "is unknown size of value returned at" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
    prettySource Loc
    ctx Loc
    loc RigidSource
    RigidRange =
      Doc ()
    "is unknown length of range at" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
    prettySource Loc
    ctx Loc
    loc (RigidOutOfScope Loc
    boundloc VName
    v) =
      Doc ()
    "is an unknown size arising from "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    v)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    " going out of scope at "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "Originally bound at "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    boundloc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
    prettySource Loc
    _ Loc
    _ RigidSource
    RigidUnify =
      Doc ()
    "is an artificial size invented during unification of functions with anonymous sizes."
    prettySource Loc
    ctx Loc
    loc (RigidCond StructType
    t1 StructType
    t2) =
      Doc ()
    "is unknown due to conditional expression at "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> Loc -> String
    forall a b. (Located a, Located b) => a -> b -> String
    locStrRel Loc
    ctx Loc
    loc)
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "One branch returns array of type: "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    align (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t1)
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "The other an array of type:       "
        Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    align (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t2)

    -- | Retrieve notes describing the purpose or origin of the given
    -- t'Size'.  The location is used as the *current* location, for the
    -- purpose of reporting relative locations.
    dimNotes :: (Located a, MonadUnify m) => a -> Exp -> m Notes
    dimNotes :: forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes a
    ctx (Var QualName VName
    d Info StructType
    _ SrcLoc
    _) = do
      Maybe (Int, Constraint)
    c <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    d) (Constraints -> Maybe (Int, Constraint))
    -> m Constraints -> m (Maybe (Int, Constraint))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      case Maybe (Int, Constraint)
    c of
        Just (Int
    _, UnknownSize Loc
    loc RigidSource
    rsrc) ->
          Notes -> m Notes
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Notes -> m Notes) -> (Doc () -> Notes) -> Doc () -> m Notes
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc () -> Notes
    aNote (Doc () -> m Notes) -> Doc () -> m Notes
    forall a b. (a -> b) -> a -> b
    $
            Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (QualName VName -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. QualName VName -> Doc ann
    pretty QualName VName
    d) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Loc -> Loc -> RigidSource -> Doc ()
    prettySource (a -> Loc
    forall a. Located a => a -> Loc
    locOf a
    ctx) Loc
    loc RigidSource
    rsrc
        Maybe (Int, Constraint)
    _ -> Notes -> m Notes
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Notes
    forall a. Monoid a => a
    mempty
    dimNotes a
    _ Exp
    _ = Notes -> m Notes
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Notes
    forall a. Monoid a => a
    mempty

    typeNotes :: (Located a, MonadUnify m) => a -> StructType -> m Notes
    typeNotes :: forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> StructType -> m Notes
    typeNotes a
    ctx =
      ([Notes] -> Notes) -> m [Notes] -> m Notes
    forall a b. (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    fmap [Notes] -> Notes
    forall a. Monoid a => [a] -> a
    mconcat
        (m [Notes] -> m Notes)
    -> (StructType -> m [Notes]) -> StructType -> m Notes
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (VName -> m Notes) -> [VName] -> m [Notes]
    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 (a -> Exp -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes a
    ctx (Exp -> m Notes) -> (VName -> Exp) -> VName -> m Notes
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (QualName VName -> SrcLoc -> Exp)
    -> SrcLoc -> QualName VName -> Exp
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip QualName VName -> SrcLoc -> Exp
    sizeFromName SrcLoc
    forall a. Monoid a => a
    mempty (QualName VName -> Exp)
    -> (VName -> QualName VName) -> VName -> Exp
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VName -> QualName VName
    forall v. v -> QualName v
    qualName)
        ([VName] -> m [Notes])
    -> (StructType -> [VName]) -> StructType -> m [Notes]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set VName -> [VName]
    forall a. Set a -> [a]
    S.toList
        (Set VName -> [VName])
    -> (StructType -> Set VName) -> StructType -> [VName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . FV -> Set VName
    fvVars
        (FV -> Set VName) -> (StructType -> FV) -> StructType -> Set VName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . StructType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType

    typeVarNotes :: (MonadUnify m) => VName -> m Notes
    typeVarNotes :: forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    v = Notes
    -> ((Int, Constraint) -> Notes) -> Maybe (Int, Constraint) -> Notes
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Notes
    forall a. Monoid a => a
    mempty (Constraint -> Notes
    note (Constraint -> Notes)
    -> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Notes
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int, Constraint) -> Constraint
    forall a b. (a, b) -> b
    snd) (Maybe (Int, Constraint) -> Notes)
    -> (Constraints -> Maybe (Int, Constraint)) -> Constraints -> Notes
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v (Constraints -> Notes) -> m Constraints -> m Notes
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      where
        note :: Constraint -> Notes
    note (HasConstrs Liftedness
    _ Map Name [StructType]
    cs Usage
    _) =
          Doc () -> Notes
    aNote (Doc () -> Notes) -> Doc () -> Notes
    forall a b. (a -> b) -> a -> b
    $
            VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    v
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "="
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    hsep (((Name, [StructType]) -> Doc ())
    -> [(Name, [StructType])] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, [StructType]) -> Doc ()
    forall {a} {b} {ann}. Pretty a => (a, b) -> Doc ann
    ppConstr (Map Name [StructType] -> [(Name, [StructType])]
    forall k a. Map k a -> [(k, a)]
    M.toList Map Name [StructType]
    cs))
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "..."
        note (Overloaded [PrimType]
    ts Usage
    _) =
          Doc () -> Notes
    aNote (Doc () -> Notes) -> Doc () -> Notes
    forall a b. (a -> b) -> a -> b
    $ VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    v Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "must be one of" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. Monoid a => [a] -> a
    mconcat (Doc () -> [Doc ()] -> [Doc ()]
    forall ann. Doc ann -> [Doc ann] -> [Doc ann]
    punctuate Doc ()
    ", " ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts))
        note (HasFields Liftedness
    _ Map Name StructType
    fs Usage
    _) =
          Doc () -> Notes
    aNote (Doc () -> Notes) -> Doc () -> Notes
    forall a b. (a -> b) -> a -> b
    $
            VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    v
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "="
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    braces ([Doc ()] -> Doc ()
    forall a. Monoid a => [a] -> a
    mconcat (Doc () -> [Doc ()] -> [Doc ()]
    forall ann. Doc ann -> [Doc ann] -> [Doc ann]
    punctuate Doc ()
    ", " (((Name, StructType) -> Doc ()) -> [(Name, StructType)] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map (Name, StructType) -> Doc ()
    forall {v} {b} {a}. IsName v => (v, b) -> Doc a
    ppField (Map Name StructType -> [(Name, StructType)]
    forall k a. Map k a -> [(k, a)]
    M.toList Map Name StructType
    fs))))
        note Constraint
    _ = Notes
    forall a. Monoid a => a
    mempty

        ppConstr :: (a, b) -> Doc ann
    ppConstr (a
    c, b
    _) = Doc ann
    "#" Doc ann -> Doc ann -> Doc ann
    forall a. Semigroup a => a -> a -> a
    <> a -> Doc ann
    forall ann. a -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty a
    c Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ann
    "..." Doc ann -> Doc ann -> Doc ann
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ann
    "|"
        ppField :: (v, b) -> Doc a
    ppField (v
    f, b
    _) = v -> Doc a
    forall a. v -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName v
    f Doc a -> Doc a -> Doc a
    forall a. Semigroup a => a -> a -> a
    <> Doc a
    ":" Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc a
    "..."

    -- | Monads that which to perform unification must implement this type
    -- class.
    class (Monad m) => MonadUnify m where
      getConstraints :: m Constraints
      putConstraints :: Constraints -> m ()
      modifyConstraints :: (Constraints -> Constraints) -> m ()
      modifyConstraints Constraints -> Constraints
    f = do
        Constraints
    x <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
        Constraints -> m ()
    forall (m :: * -> *). MonadUnify m => Constraints -> m ()
    putConstraints (Constraints -> m ()) -> Constraints -> m ()
    forall a b. (a -> b) -> a -> b
    $ Constraints -> Constraints
    f Constraints
    x

      newTypeVar :: (Monoid als, Located a) => a -> Name -> m (TypeBase dim als)
      newDimVar :: Usage -> Rigidity -> Name -> m VName
      newRigidDim :: (Located a) => a -> RigidSource -> Name -> m VName
      newRigidDim a
    loc = Usage -> Rigidity -> Name -> m VName
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> Rigidity -> Name -> m VName
    newDimVar (a -> Usage
    forall a. Located a => a -> Usage
    mkUsage' a
    loc) (Rigidity -> Name -> m VName)
    -> (RigidSource -> Rigidity) -> RigidSource -> Name -> m VName
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . RigidSource -> Rigidity
    Rigid
      newFlexibleDim :: Usage -> Name -> m VName
      newFlexibleDim Usage
    usage = Usage -> Rigidity -> Name -> m VName
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> Rigidity -> Name -> m VName
    newDimVar Usage
    usage Rigidity
    Nonrigid

      curLevel :: m Level

      matchError ::
        (Located loc) =>
        loc ->
        Notes ->
        BreadCrumbs ->
        StructType ->
        StructType ->
        m a

      unifyError ::
        (Located loc) =>
        loc ->
        Notes ->
        BreadCrumbs ->
        Doc () ->
        m a

    -- | Replace all type variables with their substitution.
    normTypeFully :: (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully :: forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully a
    t = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      a -> m a
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (a -> m a) -> a -> m a
    forall a b. (a -> b) -> a -> b
    $ TypeSubs -> a -> a
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
    `lookupSubst` Constraints
    constraints) a
    t

    -- | Replace any top-level type variable with its substitution.
    normType :: (MonadUnify m) => StructType -> m StructType
    normType :: forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType t :: StructType
    t@(Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v) [])) = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      case (Int, Constraint) -> Constraint
    forall a b. (a, b) -> b
    snd ((Int, Constraint) -> Constraint)
    -> Maybe (Int, Constraint) -> Maybe Constraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints of
        Just (Constraint (RetType [] StructType
    t') Usage
    _) -> StructType -> m StructType
    forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType StructType
    t'
        Maybe Constraint
    _ -> StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    t
    normType StructType
    t = StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    t

    rigidConstraint :: Constraint -> Bool
    rigidConstraint :: Constraint -> Bool
    rigidConstraint ParamType {} = Bool
    True
    rigidConstraint ParamSize {} = Bool
    True
    rigidConstraint UnknownSize {} = Bool
    True
    rigidConstraint Constraint
    _ = Bool
    False

    unsharedConstructorsMsg :: M.Map Name t -> M.Map Name t -> Doc a
    unsharedConstructorsMsg :: forall t a. Map Name t -> Map Name t -> Doc a
    unsharedConstructorsMsg Map Name t
    cs1 Map Name t
    cs2 =
      Doc a
    "Unshared constructors:" Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc a] -> Doc a
    forall a. [Doc a] -> Doc a
    commasep ((Name -> Doc a) -> [Name] -> [Doc a]
    forall a b. (a -> b) -> [a] -> [b]
    map ((Doc a
    "#" <>) (Doc a -> Doc a) -> (Name -> Doc a) -> Name -> Doc a
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Name -> Doc a
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty) [Name]
    missing) Doc a -> Doc a -> Doc a
    forall a. Semigroup a => a -> a -> a
    <> Doc a
    "."
      where
        missing :: [Name]
    missing =
          (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Map Name t -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name t
    cs1) (Map Name t -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name t
    cs2)
            [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Map Name t -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name t
    cs2) (Map Name t -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name t
    cs1)

    -- | Is the given type variable the name of an abstract type or type
    -- parameter, which we cannot substitute?
    isRigid :: VName -> Constraints -> Bool
    isRigid :: VName -> Constraints -> Bool
    isRigid VName
    v Constraints
    constraints =
      Bool
    -> ((Int, Constraint) -> Bool) -> Maybe (Int, Constraint) -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    True (Constraint -> Bool
    rigidConstraint (Constraint -> Bool)
    -> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Int, Constraint) -> Constraint
    forall a b. (a, b) -> b
    snd) (Maybe (Int, Constraint) -> Bool)
    -> Maybe (Int, Constraint) -> Bool
    forall a b. (a -> b) -> a -> b
    $ VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints

    -- | If the given type variable is nonrigid, what is its level?
    isNonRigid :: VName -> Constraints -> Maybe Level
    isNonRigid :: VName -> Constraints -> Maybe Int
    isNonRigid VName
    v Constraints
    constraints = do
      (Int
    lvl, Constraint
    c) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints
      Bool -> Maybe ()
    forall (f :: * -> *). Alternative f => Bool -> f ()
    guard (Bool -> Maybe ()) -> Bool -> Maybe ()
    forall a b. (a -> b) -> a -> b
    $ Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ Constraint -> Bool
    rigidConstraint Constraint
    c
      Int -> Maybe Int
    forall a. a -> Maybe a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Int
    lvl

    type UnifySizes m =
      BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Exp -> Exp -> m ()

    flipUnifySizes :: UnifySizes m -> UnifySizes m
    flipUnifySizes :: forall (m :: * -> *). UnifySizes m -> UnifySizes m
    flipUnifySizes UnifySizes m
    onDims BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid Exp
    t1 Exp
    t2 =
      UnifySizes m
    onDims BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid Exp
    t2 Exp
    t1

    unifyWith ::
      (MonadUnify m) =>
      UnifySizes m ->
      Usage ->
      [VName] ->
      BreadCrumbs ->
      StructType ->
      StructType ->
      m ()
    unifyWith :: forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith UnifySizes m
    onDims Usage
    usage = Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify Bool
    False
      where
        swap :: Bool -> a -> a -> (a, a)
    swap Bool
    True a
    x a
    y = (a
    y, a
    x)
        swap Bool
    False a
    x a
    y = (a
    x, a
    y)

        subunify :: Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify Bool
    ord [VName]
    bound BreadCrumbs
    bcs StructType
    t1 StructType
    t2 = do
          Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints

          StructType
    t1' <- StructType -> m StructType
    forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType StructType
    t1
          StructType
    t2' <- StructType -> m StructType
    forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType StructType
    t2

          let nonrigid :: VName -> Maybe Int
    nonrigid VName
    v = VName -> Constraints -> Maybe Int
    isNonRigid VName
    v Constraints
    constraints

              failure :: m a
    failure = SrcLoc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> StructType -> StructType -> m a
    matchError (Usage -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf Usage
    usage) Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs StructType
    t1' StructType
    t2'

              link :: Bool -> VName -> Int -> StructType -> m ()
    link Bool
    ord' =
                UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> VName
    -> Int
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> VName
    -> Int
    -> StructType
    -> m ()
    linkVarToType UnifySizes m
    linkDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs
                where
                  -- We may have to flip the order of future calls to
                  -- onDims inside linkVarToType.
                  linkDims :: UnifySizes m
    linkDims
                    | Bool
    ord' = UnifySizes m -> UnifySizes m
    forall (m :: * -> *). UnifySizes m -> UnifySizes m
    flipUnifySizes UnifySizes m
    onDims
                    | Bool
    otherwise = UnifySizes m
    onDims

              unifyTypeArg :: BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
    unifyTypeArg BreadCrumbs
    bcs' (TypeArgDim Exp
    d1) (TypeArgDim Exp
    d2) =
                BreadCrumbs -> (Exp, Exp) -> m ()
    onDims' BreadCrumbs
    bcs' (Bool -> Exp -> Exp -> (Exp, Exp)
    forall {a}. Bool -> a -> a -> (a, a)
    swap Bool
    ord Exp
    d1 Exp
    d2)
              unifyTypeArg BreadCrumbs
    bcs' (TypeArgType StructType
    t) (TypeArgType StructType
    arg_t) =
                Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify Bool
    ord [VName]
    bound BreadCrumbs
    bcs' StructType
    t StructType
    arg_t
              unifyTypeArg BreadCrumbs
    bcs' TypeArg Exp
    _ TypeArg Exp
    _ =
                Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError
                  Usage
    usage
                  Notes
    forall a. Monoid a => a
    mempty
                  BreadCrumbs
    bcs'
                  Doc ()
    "Cannot unify a type argument with a dimension argument (or vice versa)."

              onDims' :: BreadCrumbs -> (Exp, Exp) -> m ()
    onDims' BreadCrumbs
    bcs' (Exp
    d1, Exp
    d2) =
                UnifySizes m
    onDims
                  BreadCrumbs
    bcs'
                  [VName]
    bound
                  VName -> Maybe Int
    nonrigid
                  (TypeSubs -> Exp -> Exp
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
    `lookupSubst` Constraints
    constraints) Exp
    d1)
                  (TypeSubs -> Exp -> Exp
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
    `lookupSubst` Constraints
    constraints) Exp
    d2)

          case (StructType
    t1', StructType
    t2') of
            (Scalar (Prim PrimType
    pt1), Scalar (Prim PrimType
    pt2))
              | PrimType
    pt1 PrimType -> PrimType -> Bool
    forall a. Eq a => a -> a -> Bool
    == PrimType
    pt2 -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            ( Scalar (Record Map Name StructType
    fs),
              Scalar (Record Map Name StructType
    arg_fs)
              )
                | Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    fs [Name] -> [Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    arg_fs ->
                    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    unifySharedFields UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name StructType
    fs Map Name StructType
    arg_fs
                | Bool
    otherwise -> do
                    let missing :: [Name]
    missing =
                          (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    arg_fs) (Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    fs)
                            [Name] -> [Name] -> [Name]
    forall a. [a] -> [a] -> [a]
    ++ (Name -> Bool) -> [Name] -> [Name]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (Name -> [Name] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    fs) (Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    arg_fs)
                    Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                      Doc ()
    "Unshared fields:" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((Name -> Doc ()) -> [Name] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map Name -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty [Name]
    missing) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
            ( Scalar (TypeVar NoUniqueness
    _ (QualName [VName]
    _ VName
    tn) [TypeArg Exp]
    targs),
              Scalar (TypeVar NoUniqueness
    _ (QualName [VName]
    _ VName
    arg_tn) [TypeArg Exp]
    arg_targs)
              )
                | VName
    tn VName -> VName -> Bool
    forall a. Eq a => a -> a -> Bool
    == VName
    arg_tn,
                  [TypeArg Exp] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TypeArg Exp]
    targs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [TypeArg Exp] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [TypeArg Exp]
    arg_targs -> do
                    let bcs' :: BreadCrumbs
    bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb (Doc () -> BreadCrumb
    Matching Doc ()
    "When matching type arguments.") BreadCrumbs
    bcs
                    (TypeArg Exp -> TypeArg Exp -> m ())
    -> [TypeArg Exp] -> [TypeArg Exp] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (BreadCrumbs -> TypeArg Exp -> TypeArg Exp -> m ()
    unifyTypeArg BreadCrumbs
    bcs') [TypeArg Exp]
    targs [TypeArg Exp]
    arg_targs
            ( Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v1) []),
              Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v2) [])
              ) ->
                case (VName -> Maybe Int
    nonrigid VName
    v1, VName -> Maybe Int
    nonrigid VName
    v2) of
                  (Maybe Int
    Nothing, Maybe Int
    Nothing) -> m ()
    forall {a}. m a
    failure
                  (Just Int
    lvl1, Maybe Int
    Nothing) -> Bool -> VName -> Int -> StructType -> m ()
    link Bool
    ord VName
    v1 Int
    lvl1 StructType
    t2'
                  (Maybe Int
    Nothing, Just Int
    lvl2) -> Bool -> VName -> Int -> StructType -> m ()
    link (Bool -> Bool
    not Bool
    ord) VName
    v2 Int
    lvl2 StructType
    t1'
                  (Just Int
    lvl1, Just Int
    lvl2)
                    | Int
    lvl1 Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    <= Int
    lvl2 -> Bool -> VName -> Int -> StructType -> m ()
    link Bool
    ord VName
    v1 Int
    lvl1 StructType
    t2'
                    | Bool
    otherwise -> Bool -> VName -> Int -> StructType -> m ()
    link (Bool -> Bool
    not Bool
    ord) VName
    v2 Int
    lvl2 StructType
    t1'
            (Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v1) []), StructType
    _)
              | Just Int
    lvl <- VName -> Maybe Int
    nonrigid VName
    v1 ->
                  Bool -> VName -> Int -> StructType -> m ()
    link Bool
    ord VName
    v1 Int
    lvl StructType
    t2'
            (StructType
    _, Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v2) []))
              | Just Int
    lvl <- VName -> Maybe Int
    nonrigid VName
    v2 ->
                  Bool -> VName -> Int -> StructType -> m ()
    link (Bool -> Bool
    not Bool
    ord) VName
    v2 Int
    lvl StructType
    t1'
            ( Scalar (Arrow NoUniqueness
    _ PName
    p1 Diet
    d1 StructType
    a1 (RetType [VName]
    b1_dims TypeBase Exp Uniqueness
    b1)),
              Scalar (Arrow NoUniqueness
    _ PName
    p2 Diet
    d2 StructType
    a2 (RetType [VName]
    b2_dims TypeBase Exp Uniqueness
    b2))
              )
                | (Diet -> Diet -> Bool) -> (Diet, Diet) -> Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Diet -> Diet -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) ((Diet, Diet) -> Bool) -> (Diet, Diet) -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Diet -> Diet -> (Diet, Diet)
    forall {a}. Bool -> a -> a -> (a, a)
    swap Bool
    ord Diet
    d1 Diet
    d2 -> do
                    Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    withIndexLink Doc ()
    "unify-consuming-param" (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                      Doc ()
    "Parameters"
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (Diet -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Diet -> Doc ann
    pretty Diet
    d1 Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    a1)
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "and"
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (Diet -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Diet -> Doc ann
    pretty Diet
    d2 Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    a2)
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "are incompatible regarding consuming their arguments."
                | (Uniqueness -> Uniqueness -> Bool)
    -> (Uniqueness, Uniqueness) -> Bool
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry Uniqueness -> Uniqueness -> Bool
    forall a. Ord a => a -> a -> Bool
    (<) ((Uniqueness, Uniqueness) -> Bool)
    -> (Uniqueness, Uniqueness) -> Bool
    forall a b. (a -> b) -> a -> b
    $ Bool -> Uniqueness -> Uniqueness -> (Uniqueness, Uniqueness)
    forall {a}. Bool -> a -> a -> (a, a)
    swap Bool
    ord (TypeBase Exp Uniqueness -> Uniqueness
    forall shape. TypeBase shape Uniqueness -> Uniqueness
    uniqueness TypeBase Exp Uniqueness
    b2) (TypeBase Exp Uniqueness -> Uniqueness
    forall shape. TypeBase shape Uniqueness -> Uniqueness
    uniqueness TypeBase Exp Uniqueness
    b1) -> do
                    Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> (Doc () -> Doc ()) -> Doc () -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    withIndexLink Doc ()
    "unify-return-uniqueness" (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                      Doc ()
    "Return types"
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (TypeBase Exp Uniqueness -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase Exp Uniqueness -> Doc ann
    pretty TypeBase Exp Uniqueness
    b1)
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "and"
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (TypeBase Exp Uniqueness -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase Exp Uniqueness -> Doc ann
    pretty TypeBase Exp Uniqueness
    b2)
                        Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "have incompatible uniqueness."
                | Bool
    otherwise -> do
                    -- Introduce the existentials as size variables so they
                    -- are subject to unification.  We will remove them again
                    -- afterwards.
                    let (Constraint
    r1, Constraint
    r2) =
                          Bool -> Constraint -> Constraint -> (Constraint, Constraint)
    forall {a}. Bool -> a -> a -> (a, a)
    swap
                            Bool
    ord
                            (Maybe Exp -> Usage -> Constraint
    Size Maybe Exp
    forall a. Maybe a
    Nothing (Usage -> Constraint) -> Usage -> Constraint
    forall a b. (a -> b) -> a -> b
    $ Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing Loc
    forall a. Monoid a => a
    mempty)
                            (Loc -> RigidSource -> Constraint
    UnknownSize Loc
    forall a. Monoid a => a
    mempty RigidSource
    RigidUnify)
                    Int
    lvl <- m Int
    forall (m :: * -> *). MonadUnify m => m Int
    curLevel
                    (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ([(VName, (Int, Constraint))] -> Constraints
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ((VName -> (VName, (Int, Constraint)))
    -> [VName] -> [(VName, (Int, Constraint))]
    forall a b. (a -> b) -> [a] -> [b]
    map (,(Int
    lvl, Constraint
    r1)) [VName]
    b1_dims) <>)
                    (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ([(VName, (Int, Constraint))] -> Constraints
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ((VName -> (VName, (Int, Constraint)))
    -> [VName] -> [(VName, (Int, Constraint))]
    forall a b. (a -> b) -> [a] -> [b]
    map (,(Int
    lvl, Constraint
    r2)) [VName]
    b2_dims) <>)

                    let bound' :: [VName]
    bound' = [VName]
    bound [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> (PName -> Maybe VName) -> [PName] -> [VName]
    forall a b. (a -> Maybe b) -> [a] -> [b]
    mapMaybe PName -> Maybe VName
    pname [PName
    p1, PName
    p2] [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> [VName]
    b1_dims [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> [VName]
    b2_dims
                    Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify
                      (Bool -> Bool
    not Bool
    ord)
                      [VName]
    bound
                      (BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb (Doc () -> BreadCrumb
    Matching Doc ()
    "When matching parameter types.") BreadCrumbs
    bcs)
                      StructType
    a1
                      StructType
    a2
                    Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify
                      Bool
    ord
                      [VName]
    bound'
                      (BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb (Doc () -> BreadCrumb
    Matching Doc ()
    "When matching return types.") BreadCrumbs
    bcs)
                      (TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    b1')
                      (TypeBase Exp Uniqueness -> StructType
    forall dim u. TypeBase dim u -> TypeBase dim NoUniqueness
    toStruct TypeBase Exp Uniqueness
    b2')

                    -- Delete the size variables we introduced to represent
                    -- the existential sizes.
                    (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \Constraints
    m -> (Constraints -> VName -> Constraints)
    -> Constraints -> [VName] -> Constraints
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    L.foldl' ((VName -> Constraints -> Constraints)
    -> Constraints -> VName -> Constraints
    forall a b c. (a -> b -> c) -> b -> a -> c
    flip VName -> Constraints -> Constraints
    forall k a. Ord k => k -> Map k a -> Map k a
    M.delete) Constraints
    m ([VName]
    b1_dims [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> [VName]
    b2_dims)
                where
                  (TypeBase Exp Uniqueness
    b1', TypeBase Exp Uniqueness
    b2') =
                    -- Replace one parameter name with the other in the
                    -- return type, in case of dependent types.  I.e.,
                    -- we want type '(n: i32) -> [n]i32' to unify with
                    -- type '(x: i32) -> [x]i32'.
                    case (PName
    p1, PName
    p2) of
                      (Named VName
    p1', Named VName
    p2') ->
                        let f :: VName -> Maybe (Subst t)
    f VName
    v
                              | VName
    v VName -> VName -> Bool
    forall a. Eq a => a -> a -> Bool
    == VName
    p2' = Subst t -> Maybe (Subst t)
    forall a. a -> Maybe a
    Just (Subst t -> Maybe (Subst t)) -> Subst t -> Maybe (Subst t)
    forall a b. (a -> b) -> a -> b
    $ Exp -> Subst t
    forall t. Exp -> Subst t
    ExpSubst (Exp -> Subst t) -> Exp -> Subst t
    forall a b. (a -> b) -> a -> b
    $ QualName VName -> SrcLoc -> Exp
    sizeFromName (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    p1') SrcLoc
    forall a. Monoid a => a
    mempty
                              | Bool
    otherwise = Maybe (Subst t)
    forall a. Maybe a
    Nothing
                         in (TypeBase Exp Uniqueness
    b1, TypeSubs -> TypeBase Exp Uniqueness -> TypeBase Exp Uniqueness
    forall a. Substitutable a => TypeSubs -> a -> a
    applySubst TypeSubs
    forall {t}. VName -> Maybe (Subst t)
    f TypeBase Exp Uniqueness
    b2)
                      (PName
    _, PName
    _) ->
                        (TypeBase Exp Uniqueness
    b1, TypeBase Exp Uniqueness
    b2)

                  pname :: PName -> Maybe VName
    pname (Named VName
    x) = VName -> Maybe VName
    forall a. a -> Maybe a
    Just VName
    x
                  pname PName
    Unnamed = Maybe VName
    forall a. Maybe a
    Nothing
            (Array {}, Array {})
              | Shape (Exp
    t1_d : [Exp]
    _) <- StructType -> Shape Exp
    forall dim as. TypeBase dim as -> Shape dim
    arrayShape StructType
    t1',
                Shape (Exp
    t2_d : [Exp]
    _) <- StructType -> Shape Exp
    forall dim as. TypeBase dim as -> Shape dim
    arrayShape StructType
    t2',
                Just StructType
    t1'' <- Int -> StructType -> Maybe StructType
    forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
    peelArray Int
    1 StructType
    t1',
                Just StructType
    t2'' <- Int -> StructType -> Maybe StructType
    forall dim u. Int -> TypeBase dim u -> Maybe (TypeBase dim u)
    peelArray Int
    1 StructType
    t2' -> do
                  BreadCrumbs -> (Exp, Exp) -> m ()
    onDims' BreadCrumbs
    bcs (Bool -> Exp -> Exp -> (Exp, Exp)
    forall {a}. Bool -> a -> a -> (a, a)
    swap Bool
    ord Exp
    t1_d Exp
    t2_d)
                  Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
    subunify Bool
    ord [VName]
    bound BreadCrumbs
    bcs StructType
    t1'' StructType
    t2''
            ( Scalar (Sum Map Name [StructType]
    cs),
              Scalar (Sum Map Name [StructType]
    arg_cs)
              )
                | Map Name [StructType] -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name [StructType]
    cs [Name] -> [Name] -> Bool
    forall a. Eq a => a -> a -> Bool
    == Map Name [StructType] -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name [StructType]
    arg_cs ->
                    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    unifySharedConstructors UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name [StructType]
    cs Map Name [StructType]
    arg_cs
                | Bool
    otherwise ->
                    Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Map Name [StructType] -> Map Name [StructType] -> Doc ()
    forall t a. Map Name t -> Map Name t -> Doc a
    unsharedConstructorsMsg Map Name [StructType]
    arg_cs Map Name [StructType]
    cs
            (StructType, StructType)
    _ -> m ()
    forall {a}. m a
    failure

    anyBound :: [VName] -> ExpBase Info VName -> Bool
    anyBound :: [VName] -> Exp -> Bool
    anyBound [VName]
    bound Exp
    e = (VName -> Bool) -> [VName] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` FV -> Set VName
    fvVars (Exp -> FV
    freeInExp Exp
    e)) [VName]
    bound

    unifySizes :: (MonadUnify m) => Usage -> UnifySizes m
    unifySizes :: forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
    unifySizes Usage
    usage BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid Exp
    e1 Exp
    e2
      | Just [(Exp, Exp)]
    es <- Exp -> Exp -> Maybe [(Exp, Exp)]
    similarExps Exp
    e1 Exp
    e2 =
          ((Exp, Exp) -> m ()) -> [(Exp, Exp)] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
    forall a b c. (a -> b -> c) -> (a, b) -> c
    uncurry ((Exp -> Exp -> m ()) -> (Exp, Exp) -> m ())
    -> (Exp -> Exp -> m ()) -> (Exp, Exp) -> m ()
    forall a b. (a -> b) -> a -> b
    $ Usage -> UnifySizes m
    forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
    unifySizes Usage
    usage BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid) [(Exp, Exp)]
    es
    unifySizes Usage
    usage BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid (Var QualName VName
    v1 Info StructType
    _ SrcLoc
    _) Exp
    e2
      | Just Int
    lvl1 <- VName -> Maybe Int
    nonrigid (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v1),
        Bool -> Bool
    not ([VName] -> Exp -> Bool
    anyBound [VName]
    bound Exp
    e2) Bool -> Bool -> Bool
    || (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v1 VName -> [VName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [VName]
    bound) =
          Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
    linkVarToDim Usage
    usage BreadCrumbs
    bcs (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v1) Int
    lvl1 Exp
    e2
    unifySizes Usage
    usage BreadCrumbs
    bcs [VName]
    bound VName -> Maybe Int
    nonrigid Exp
    e1 (Var QualName VName
    v2 Info StructType
    _ SrcLoc
    _)
      | Just Int
    lvl2 <- VName -> Maybe Int
    nonrigid (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v2),
        Bool -> Bool
    not ([VName] -> Exp -> Bool
    anyBound [VName]
    bound Exp
    e1) Bool -> Bool -> Bool
    || (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v2 VName -> [VName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [VName]
    bound) =
          Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
    linkVarToDim Usage
    usage BreadCrumbs
    bcs (QualName VName -> VName
    forall vn. QualName vn -> vn
    qualLeaf QualName VName
    v2) Int
    lvl2 Exp
    e1
    unifySizes Usage
    usage BreadCrumbs
    bcs [VName]
    _ VName -> Maybe Int
    _ Exp
    e1 Exp
    e2 = do
      Notes
    notes <- Notes -> Notes -> Notes
    forall a. Semigroup a => a -> a -> a
    (<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Usage -> Exp -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes Usage
    usage Exp
    e2 m (Notes -> Notes) -> m Notes -> m Notes
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> Usage -> Exp -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes Usage
    usage Exp
    e2
      Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    notes BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        Doc ()
    "Sizes"
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Exp -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Exp -> Doc ann
    pretty Exp
    e1)
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "and"
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Exp -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Exp -> Doc ann
    pretty Exp
    e2)
          Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "do not match."

    -- | Unifies two types.
    unify :: (MonadUnify m) => Usage -> StructType -> StructType -> m ()
    unify :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage = UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith (Usage -> UnifySizes m
    forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
    unifySizes Usage
    usage) Usage
    usage [VName]
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs

    occursCheck ::
      (MonadUnify m) =>
      Usage ->
      BreadCrumbs ->
      VName ->
      StructType ->
      m ()
    occursCheck :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> StructType -> m ()
    occursCheck Usage
    usage BreadCrumbs
    bcs VName
    vn StructType
    tp =
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (VName
    vn VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` StructType -> Set VName
    forall dim as. TypeBase dim as -> Set VName
    typeVars StructType
    tp) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
          Doc ()
    "Occurs check: cannot instantiate"
            Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn
            Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "with"
            Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    tp
            Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."

    scopeCheck ::
      (MonadUnify m) =>
      Usage ->
      BreadCrumbs ->
      VName ->
      Level ->
      StructType ->
      m ()
    scopeCheck :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    scopeCheck Usage
    usage BreadCrumbs
    bcs VName
    vn Int
    max_lvl StructType
    tp = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      Constraints -> StructType -> m ()
    forall {m :: * -> *} {u}.
    MonadUnify m =>
    Constraints -> TypeBase Exp u -> m ()
    checkType Constraints
    constraints StructType
    tp
      where
        checkType :: Constraints -> TypeBase Exp u -> m ()
    checkType Constraints
    constraints TypeBase Exp u
    t =
          (VName -> m ()) -> Set VName -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Constraints -> VName -> m ()
    forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
    check Constraints
    constraints) (Set VName -> m ()) -> Set VName -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp u -> Set VName
    forall dim as. TypeBase dim as -> Set VName
    typeVars TypeBase Exp u
    t Set VName -> Set VName -> Set VName
    forall a. Semigroup a => a -> a -> a
    <> FV -> Set VName
    fvVars (TypeBase Exp u -> FV
    forall u. TypeBase Exp u -> FV
    freeInType TypeBase Exp u
    t)

        check :: Constraints -> VName -> m ()
    check Constraints
    constraints VName
    v
          | Just (Int
    lvl, Constraint
    c) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints,
            Int
    lvl Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    > Int
    max_lvl =
              if Constraint -> Bool
    rigidConstraint Constraint
    c
                then VName -> m ()
    forall {m :: * -> *} {v} {b}. (MonadUnify m, IsName v) => v -> m b
    scopeViolation VName
    v
                else (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    v (Int
    max_lvl, Constraint
    c)
          | Bool
    otherwise =
              () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

        scopeViolation :: v -> m b
    scopeViolation v
    v = do
          Notes
    notes <- Usage -> StructType -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> StructType -> m Notes
    typeNotes Usage
    usage StructType
    tp
          Usage -> Notes -> BreadCrumbs -> Doc () -> m b
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    notes BreadCrumbs
    bcs (Doc () -> m b) -> Doc () -> m b
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Cannot unify type"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    tp)
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "with"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "(scope violation)."
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "This is because"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (v -> Doc ()
    forall a. v -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName v
    v)
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "is rigidly bound in a deeper scope."

    -- Expressions witnessed by type, topologically sorted.
    topWit :: TypeBase Exp u -> [Exp]
    topWit :: forall u. TypeBase Exp u -> [Exp]
    topWit = (Exp -> Exp -> Bool) -> [Exp] -> [Exp]
    forall a. (a -> a -> Bool) -> [a] -> [a]
    topologicalSort Exp -> Exp -> Bool
    depends ([Exp] -> [Exp])
    -> (TypeBase Exp u -> [Exp]) -> TypeBase Exp u -> [Exp]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeBase Exp u -> [Exp]
    forall {fdim} {als}. TypeBase fdim als -> [fdim]
    witnessedExps
      where
        witnessedExps :: TypeBase fdim als -> [fdim]
    witnessedExps TypeBase fdim als
    t = State [fdim] (TypeBase () als) -> [fdim] -> [fdim]
    forall s a. State s a -> s -> s
    execState ((Set VName -> DimPos -> fdim -> StateT [fdim] Identity ())
    -> TypeBase fdim als -> State [fdim] (TypeBase () als)
    forall (f :: * -> *) fdim tdim als.
    Applicative f =>
    (Set VName -> DimPos -> fdim -> f tdim)
    -> TypeBase fdim als -> f (TypeBase tdim als)
    traverseDims Set VName -> DimPos -> fdim -> StateT [fdim] Identity ()
    forall {a} {m :: * -> *} {p}.
    MonadState [a] m =>
    p -> DimPos -> a -> m ()
    onDim TypeBase fdim als
    t) [fdim]
    forall a. Monoid a => a
    mempty
          where
            onDim :: p -> DimPos -> a -> m ()
    onDim p
    _ DimPos
    PosImmediate a
    e = ([a] -> [a]) -> m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (a
    e :)
            onDim p
    _ DimPos
    _ a
    _ = () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        depends :: Exp -> Exp -> Bool
    depends Exp
    a Exp
    b = (Exp -> Bool) -> [Exp] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (Exp -> Exp -> Bool
    sameExp Exp
    b) ([Exp] -> Bool) -> [Exp] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Exp -> [Exp]
    subExps Exp
    a

    sizeFree ::
      (MonadUnify m) =>
      SrcLoc ->
      (Exp -> Maybe VName) ->
      TypeBase Size u ->
      m (TypeBase Size u, [VName])
    sizeFree :: forall (m :: * -> *) u.
    MonadUnify m =>
    SrcLoc
    -> (Exp -> Maybe VName)
    -> TypeBase Exp u
    -> m (TypeBase Exp u, [VName])
    sizeFree SrcLoc
    tloc Exp -> Maybe VName
    expKiller TypeBase Exp u
    orig_t = do
      ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    -> [(Exp, Exp)] -> StateT [VName] m (TypeBase Exp u)
    forall r (m :: * -> *) a. ReaderT r m a -> r -> m a
    runReaderT (TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
           {m :: * -> *} {u} {b}.
    (MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
     MonadTrans t, MonadReader [(Exp, Exp)] (t (t m)), Monad (t m)) =>
    TypeBase Exp u -> t (t m) b -> t (t m) b
    toBeReplaced TypeBase Exp u
    orig_t (ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u))
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType TypeBase Exp u
    orig_t) [(Exp, Exp)]
    forall a. Monoid a => a
    mempty StateT [VName] m (TypeBase Exp u)
    -> [VName] -> m (TypeBase Exp u, [VName])
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    `runStateT` [VName]
    forall a. Monoid a => a
    mempty
      where
        lookReplacement :: Exp -> t (Exp, b) -> Maybe b
    lookReplacement Exp
    e t (Exp, b)
    repl = (Exp, b) -> b
    forall a b. (a, b) -> b
    snd ((Exp, b) -> b) -> Maybe (Exp, b) -> Maybe b
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ((Exp, b) -> Bool) -> t (Exp, b) -> Maybe (Exp, b)
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    L.find (Exp -> Exp -> Bool
    sameExp Exp
    e (Exp -> Bool) -> ((Exp, b) -> Exp) -> (Exp, b) -> Bool
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (Exp, b) -> Exp
    forall a b. (a, b) -> a
    fst) t (Exp, b)
    repl
        expReplace :: t (Exp, Exp) -> Exp -> Exp
    expReplace t (Exp, Exp)
    mapping Exp
    e
          | Just Exp
    e' <- Exp -> t (Exp, Exp) -> Maybe Exp
    forall {t :: * -> *} {b}.
    Foldable t =>
    Exp -> t (Exp, b) -> Maybe b
    lookReplacement Exp
    e t (Exp, Exp)
    mapping = Exp
    e'
          | Bool
    otherwise = Identity Exp -> Exp
    forall a. Identity a -> a
    runIdentity (Identity Exp -> Exp) -> Identity Exp -> Exp
    forall a b. (a -> b) -> a -> b
    $ ASTMapper Identity -> Exp -> Identity Exp
    forall x (m :: * -> *).
    (ASTMappable x, Monad m) =>
    ASTMapper m -> x -> m x
    forall (m :: * -> *). Monad m => ASTMapper m -> Exp -> m Exp
    astMap ASTMapper Identity
    mapper Exp
    e
          where
            mapper :: ASTMapper Identity
    mapper = ASTMapper Identity
    forall (m :: * -> *). Monad m => ASTMapper m
    identityMapper {mapOnExp = pure . expReplace mapping}

        replacing :: Exp -> t (t m) Exp
    replacing Exp
    e = do
          Exp
    e' <- (t (Exp, Exp) -> Exp) -> t (t m) Exp
    forall r (m :: * -> *) a. MonadReader r m => (r -> a) -> m a
    asks (t (Exp, Exp) -> Exp -> Exp
    forall {t :: * -> *}. Foldable t => t (Exp, Exp) -> Exp -> Exp
    `expReplace` Exp
    e)
          case Exp -> Maybe VName
    expKiller Exp
    e' of
            Maybe VName
    Nothing -> Exp -> t (t m) Exp
    forall a. a -> t (t m) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Exp
    e'
            Just VName
    cause -> do
              VName
    vn <- t m VName -> t (t m) VName
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (t m VName -> t (t m) VName) -> t m VName -> t (t m) VName
    forall a b. (a -> b) -> a -> b
    $ m VName -> t m VName
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m VName -> t m VName) -> m VName -> t m VName
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> RigidSource -> Name -> m VName
    forall a. Located a => a -> RigidSource -> Name -> m VName
    forall (m :: * -> *) a.
    (MonadUnify m, Located a) =>
    a -> RigidSource -> Name -> m VName
    newRigidDim SrcLoc
    tloc (Loc -> VName -> RigidSource
    RigidOutOfScope (Exp -> Loc
    forall a. Located a => a -> Loc
    locOf Exp
    e) VName
    cause) Name
    "d"
              ([VName] -> [VName]) -> t (t m) ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (VName
    vn :)
              Exp -> t (t m) Exp
    forall a. a -> t (t m) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Exp -> t (t m) Exp) -> Exp -> t (t m) Exp
    forall a b. (a -> b) -> a -> b
    $ QualName VName -> SrcLoc -> Exp
    sizeFromName (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    vn) (Exp -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf Exp
    e)

        toBeReplaced :: TypeBase Exp u -> t (t m) b -> t (t m) b
    toBeReplaced TypeBase Exp u
    t t (t m) b
    m' = (t (t m) b -> Exp -> t (t m) b) -> t (t m) b -> [Exp] -> t (t m) b
    forall b a. (b -> a -> b) -> b -> [a] -> b
    forall (t :: * -> *) b a.
    Foldable t =>
    (b -> a -> b) -> b -> t a -> b
    foldl t (t m) b -> Exp -> t (t m) b
    forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
           {m :: * -> *} {b}.
    (MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
     MonadTrans t, MonadReader [(Exp, Exp)] (t (t m)), Monad (t m)) =>
    t (t m) b -> Exp -> t (t m) b
    f t (t m) b
    m' ([Exp] -> t (t m) b) -> [Exp] -> t (t m) b
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp u -> [Exp]
    forall u. TypeBase Exp u -> [Exp]
    topWit TypeBase Exp u
    t
          where
            f :: t (t m) b -> Exp -> t (t m) b
    f t (t m) b
    m Exp
    e = do
              Exp
    e' <- Exp -> t (t m) Exp
    forall {t :: * -> *} {t :: (* -> *) -> * -> *}
           {t :: (* -> *) -> * -> *} {m :: * -> *}.
    (MonadReader (t (Exp, Exp)) (t (t m)), Foldable t, MonadTrans t,
     MonadTrans t, Monad (t m), MonadUnify m,
     MonadState [VName] (t (t m))) =>
    Exp -> t (t m) Exp
    replacing Exp
    e
              ([(Exp, Exp)] -> [(Exp, Exp)]) -> t (t m) b -> t (t m) b
    forall a. ([(Exp, Exp)] -> [(Exp, Exp)]) -> t (t m) a -> t (t m) a
    forall r (m :: * -> *) a. MonadReader r m => (r -> r) -> m a -> m a
    local ((Exp
    e, Exp
    e') :) t (t m) b
    m

        onScalar :: ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    onScalar (Record Map Name (TypeBase Exp u)
    fs) =
          Map Name (TypeBase Exp u) -> ScalarTypeBase Exp u
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record (Map Name (TypeBase Exp u) -> ScalarTypeBase Exp u)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (Map Name (TypeBase Exp u))
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TypeBase Exp u
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u))
    -> Map Name (TypeBase Exp u)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (Map Name (TypeBase Exp u))
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Name a -> f (Map Name b)
    traverse TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType Map Name (TypeBase Exp u)
    fs
        onScalar (Sum Map Name [TypeBase Exp u]
    cs) =
          Map Name [TypeBase Exp u] -> ScalarTypeBase Exp u
    forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
    Sum (Map Name [TypeBase Exp u] -> ScalarTypeBase Exp u)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (Map Name [TypeBase Exp u])
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (([TypeBase Exp u]
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeBase Exp u])
    -> Map Name [TypeBase Exp u]
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (Map Name [TypeBase Exp u])
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Map Name a -> f (Map Name b)
    traverse (([TypeBase Exp u]
      -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeBase Exp u])
     -> Map Name [TypeBase Exp u]
     -> ReaderT
          [(Exp, Exp)] (StateT [VName] m) (Map Name [TypeBase Exp u]))
    -> ((TypeBase Exp u
         -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u))
        -> [TypeBase Exp u]
        -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeBase Exp u])
    -> (TypeBase Exp u
        -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u))
    -> Map Name [TypeBase Exp u]
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (Map Name [TypeBase Exp u])
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . (TypeBase Exp u
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u))
    -> [TypeBase Exp u]
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeBase Exp u]
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> [a] -> f [b]
    traverse) TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType Map Name [TypeBase Exp u]
    cs
        onScalar (Arrow u
    as PName
    pn Diet
    d StructType
    argT (RetType [VName]
    dims TypeBase Exp Uniqueness
    retT)) = do
          StructType
    argT' <- StructType -> ReaderT [(Exp, Exp)] (StateT [VName] m) StructType
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType StructType
    argT
          [VName]
    old_bound <- ReaderT [(Exp, Exp)] (StateT [VName] m) [VName]
    forall s (m :: * -> *). MonadState s m => m s
    get
          TypeBase Exp Uniqueness
    retT' <- TypeBase Exp Uniqueness
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
    forall {t :: (* -> *) -> * -> *} {t :: (* -> *) -> * -> *}
           {m :: * -> *} {u} {b}.
    (MonadState [VName] (t (t m)), MonadUnify m, MonadTrans t,
     MonadTrans t, MonadReader [(Exp, Exp)] (t (t m)), Monad (t m)) =>
    TypeBase Exp u -> t (t m) b -> t (t m) b
    toBeReplaced TypeBase Exp Uniqueness
    retT (ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
     -> ReaderT
          [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness))
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
    forall a b. (a -> b) -> a -> b
    $ TypeBase Exp Uniqueness
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp Uniqueness)
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType TypeBase Exp Uniqueness
    retT
          [VName]
    rl <- ([VName] -> ([VName], [VName]))
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) [VName]
    forall a.
    ([VName] -> (a, [VName]))
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) a
    forall s (m :: * -> *) a. MonadState s m => (s -> (a, s)) -> m a
    state (([VName] -> ([VName], [VName]))
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) [VName])
    -> ([VName] -> ([VName], [VName]))
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) [VName]
    forall a b. (a -> b) -> a -> b
    $ (VName -> Bool) -> [VName] -> ([VName], [VName])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    L.partition (VName -> [VName] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` [VName]
    old_bound)
          let dims' :: [VName]
    dims' = [VName]
    dims [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> [VName]
    rl
          ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall a. a -> ReaderT [(Exp, Exp)] (StateT [VName] m) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ScalarTypeBase Exp u
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u))
    -> ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall a b. (a -> b) -> a -> b
    $ u
    -> PName
    -> Diet
    -> StructType
    -> RetTypeBase Exp Uniqueness
    -> ScalarTypeBase Exp u
    forall dim u.
    u
    -> PName
    -> Diet
    -> TypeBase dim NoUniqueness
    -> RetTypeBase dim Uniqueness
    -> ScalarTypeBase dim u
    Arrow u
    as PName
    pn Diet
    d StructType
    argT' ([VName] -> TypeBase Exp Uniqueness -> RetTypeBase Exp Uniqueness
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType [VName]
    dims' TypeBase Exp Uniqueness
    retT')
        onScalar (TypeVar u
    u QualName VName
    v [TypeArg Exp]
    args) =
          u -> QualName VName -> [TypeArg Exp] -> ScalarTypeBase Exp u
    forall dim u.
    u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
    TypeVar u
    u QualName VName
    v ([TypeArg Exp] -> ScalarTypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeArg Exp]
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (TypeArg Exp
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp))
    -> [TypeArg Exp]
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) [TypeArg Exp]
    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 TypeArg Exp
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp)
    forall {m :: * -> *}.
    MonadUnify m =>
    TypeArg Exp
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp)
    onTypeArg [TypeArg Exp]
    args
          where
            onTypeArg :: TypeArg Exp
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp)
    onTypeArg (TypeArgDim Exp
    d) = Exp -> TypeArg Exp
    forall dim. dim -> TypeArg dim
    TypeArgDim (Exp -> TypeArg Exp)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) Exp
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> Exp -> ReaderT [(Exp, Exp)] (StateT [VName] m) Exp
    forall {t :: * -> *} {t :: (* -> *) -> * -> *}
           {t :: (* -> *) -> * -> *} {m :: * -> *}.
    (MonadReader (t (Exp, Exp)) (t (t m)), Foldable t, MonadTrans t,
     MonadTrans t, Monad (t m), MonadUnify m,
     MonadState [VName] (t (t m))) =>
    Exp -> t (t m) Exp
    replacing Exp
    d
            onTypeArg (TypeArgType StructType
    ty) = StructType -> TypeArg Exp
    forall dim. TypeBase dim NoUniqueness -> TypeArg dim
    TypeArgType (StructType -> TypeArg Exp)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) StructType
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeArg Exp)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> StructType -> ReaderT [(Exp, Exp)] (StateT [VName] m) StructType
    forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType StructType
    ty
        onScalar (Prim PrimType
    pt) = ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall a. a -> ReaderT [(Exp, Exp)] (StateT [VName] m) a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (ScalarTypeBase Exp u
     -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u))
    -> ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall a b. (a -> b) -> a -> b
    $ PrimType -> ScalarTypeBase Exp u
    forall dim u. PrimType -> ScalarTypeBase dim u
    Prim PrimType
    pt

        onType ::
          (MonadUnify m) =>
          TypeBase Size u ->
          ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Size u)
        onType :: forall (m :: * -> *) u.
    MonadUnify m =>
    TypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    onType (Array u
    u Shape Exp
    shape ScalarTypeBase Exp NoUniqueness
    scalar) =
          u -> Shape Exp -> ScalarTypeBase Exp NoUniqueness -> TypeBase Exp u
    forall dim u.
    u -> Shape dim -> ScalarTypeBase dim NoUniqueness -> TypeBase dim u
    Array u
    u (Shape Exp -> ScalarTypeBase Exp NoUniqueness -> TypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (Shape Exp)
    -> ReaderT
         [(Exp, Exp)]
         (StateT [VName] m)
         (ScalarTypeBase Exp NoUniqueness -> TypeBase Exp u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> (Exp -> ReaderT [(Exp, Exp)] (StateT [VName] m) Exp)
    -> Shape Exp -> ReaderT [(Exp, Exp)] (StateT [VName] m) (Shape Exp)
    forall (t :: * -> *) (f :: * -> *) a b.
    (Traversable t, Applicative f) =>
    (a -> f b) -> t a -> f (t b)
    forall (f :: * -> *) a b.
    Applicative f =>
    (a -> f b) -> Shape a -> f (Shape b)
    traverse Exp -> ReaderT [(Exp, Exp)] (StateT [VName] m) Exp
    forall {t :: * -> *} {t :: (* -> *) -> * -> *}
           {t :: (* -> *) -> * -> *} {m :: * -> *}.
    (MonadReader (t (Exp, Exp)) (t (t m)), Foldable t, MonadTrans t,
     MonadTrans t, Monad (t m), MonadUnify m,
     MonadState [VName] (t (t m))) =>
    Exp -> t (t m) Exp
    replacing Shape Exp
    shape ReaderT
      [(Exp, Exp)]
      (StateT [VName] m)
      (ScalarTypeBase Exp NoUniqueness -> TypeBase Exp u)
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp NoUniqueness)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall a b.
    ReaderT [(Exp, Exp)] (StateT [VName] m) (a -> b)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) a
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> ScalarTypeBase Exp NoUniqueness
    -> ReaderT
         [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp NoUniqueness)
    forall {m :: * -> *} {u}.
    MonadUnify m =>
    ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    onScalar ScalarTypeBase Exp NoUniqueness
    scalar
        onType (Scalar ScalarTypeBase Exp u
    ty) =
          ScalarTypeBase Exp u -> TypeBase Exp u
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp u -> TypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Exp u)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    forall {m :: * -> *} {u}.
    MonadUnify m =>
    ScalarTypeBase Exp u
    -> ReaderT [(Exp, Exp)] (StateT [VName] m) (ScalarTypeBase Exp u)
    onScalar ScalarTypeBase Exp u
    ty

    linkVarToType ::
      (MonadUnify m) =>
      UnifySizes m ->
      Usage ->
      [VName] ->
      BreadCrumbs ->
      VName ->
      Level ->
      StructType ->
      m ()
    linkVarToType :: forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> VName
    -> Int
    -> StructType
    -> m ()
    linkVarToType UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs VName
    vn Int
    lvl StructType
    tp_unnorm = do
      -- We have to expand anyway for the occurs check, so we might as
      -- well link the fully expanded type.
      StructType
    tp <- StructType -> m StructType
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully StructType
    tp_unnorm
      Usage -> BreadCrumbs -> VName -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> StructType -> m ()
    occursCheck Usage
    usage BreadCrumbs
    bcs VName
    vn StructType
    tp
      Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    scopeCheck Usage
    usage BreadCrumbs
    bcs VName
    vn Int
    lvl StructType
    tp

      let link :: m ()
    link = do
            let (Set VName
    witnessed, Set VName
    not_witnessed) = StructType -> (Set VName, Set VName)
    determineSizeWitnesses StructType
    tp
                used :: VName -> Bool
    used VName
    v = VName
    v VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set VName
    witnessed Bool -> Bool -> Bool
    || VName
    v VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` Set VName
    not_witnessed
                ([VName]
    ext_witnessed, [VName]
    ext_not_witnessed) =
                  (VName -> Bool) -> [VName] -> ([VName], [VName])
    forall a. (a -> Bool) -> [a] -> ([a], [a])
    L.partition (VName -> Set VName -> Bool
    forall a. Eq a => a -> Set a -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` Set VName
    witnessed) ([VName] -> ([VName], [VName])) -> [VName] -> ([VName], [VName])
    forall a b. (a -> b) -> a -> b
    $ (VName -> Bool) -> [VName] -> [VName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter VName -> Bool
    used [VName]
    bound

                -- Any size that uses an ext_not_witnessed variable must
                -- be replaced with a fresh existential.
                problematic :: Exp -> Maybe VName
    problematic Exp
    e =
                  (VName -> Bool) -> [VName] -> Maybe VName
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
    L.find (VName -> [VName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [VName]
    ext_not_witnessed) ([VName] -> Maybe VName) -> [VName] -> Maybe VName
    forall a b. (a -> b) -> a -> b
    $
                    Set VName -> [VName]
    forall a. Set a -> [a]
    S.toList (Set VName -> [VName]) -> Set VName -> [VName]
    forall a b. (a -> b) -> a -> b
    $
                      FV -> Set VName
    fvVars (FV -> Set VName) -> FV -> Set VName
    forall a b. (a -> b) -> a -> b
    $
                        Exp -> FV
    freeInExp Exp
    e

            (StructType
    tp', [VName]
    ext_new) <- SrcLoc
    -> (Exp -> Maybe VName) -> StructType -> m (StructType, [VName])
    forall (m :: * -> *) u.
    MonadUnify m =>
    SrcLoc
    -> (Exp -> Maybe VName)
    -> TypeBase Exp u
    -> m (TypeBase Exp u, [VName])
    sizeFree (Usage -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf Usage
    usage) Exp -> Maybe VName
    problematic StructType
    tp

            (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
              VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, StructRetType -> Usage -> Constraint
    Constraint ([VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType ([VName]
    ext_new [VName] -> [VName] -> [VName]
    forall a. Semigroup a => a -> a -> a
    <> [VName]
    ext_witnessed) StructType
    tp') Usage
    usage)

      let unliftedBcs :: a -> BreadCrumbs
    unliftedBcs a
    unlifted_usage =
            BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb
              ( Doc () -> BreadCrumb
    Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
    forall a b. (a -> b) -> a -> b
    $
                  Doc ()
    "When verifying that"
                    Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                    Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Text -> Doc ()
    forall a. Text -> Doc a
    textwrap Text
    "is not instantiated with a function type, due to"
                    Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> a -> Doc ()
    forall ann. a -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty a
    unlifted_usage
              )
              BreadCrumbs
    bcs

      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      case (Int, Constraint) -> Constraint
    forall a b. (a, b) -> b
    snd ((Int, Constraint) -> Constraint)
    -> Maybe (Int, Constraint) -> Maybe Constraint
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    vn Constraints
    constraints of
        Just (NoConstraint Liftedness
    Unlifted Usage
    unlift_usage) -> do
          m ()
    link

          Usage -> BreadCrumbs -> StructType -> m ()
    forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    arrayElemTypeWith Usage
    usage (Usage -> BreadCrumbs
    forall {a}. Pretty a => a -> BreadCrumbs
    unliftedBcs Usage
    unlift_usage) StructType
    tp
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when ((VName -> Bool) -> Set VName -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    any (VName -> [VName] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [VName]
    bound) (FV -> Set VName
    fvVars (StructType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType StructType
    tp))) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
            Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
              Doc ()
    "Type variable"
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "cannot be instantiated with type containing anonymous sizes:"
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    tp)
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Text -> Doc ()
    forall a. Text -> Doc a
    textwrap Text
    "This is usually because the size of an array returned by a higher-order function argument cannot be determined statically.  This can also be due to the return size being a value parameter.  Add type annotation to clarify."
        Just (Equality Usage
    _) -> do
          m ()
    link
          Usage -> StructType -> m ()
    forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> TypeBase dim u -> m ()
    equalityType Usage
    usage StructType
    tp
        Just (Overloaded [PrimType]
    ts Usage
    old_usage)
          | StructType
    tp StructType -> [StructType] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `notElem` (PrimType -> StructType) -> [PrimType] -> [StructType]
    forall a b. (a -> b) -> [a] -> [b]
    map (ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
    -> (PrimType -> ScalarTypeBase Exp NoUniqueness)
    -> PrimType
    -> StructType
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . PrimType -> ScalarTypeBase Exp NoUniqueness
    forall dim u. PrimType -> ScalarTypeBase dim u
    Prim) [PrimType]
    ts -> do
              m ()
    link
              case StructType
    tp of
                Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v) [])
                  | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ VName -> Constraints -> Bool
    isRigid VName
    v Constraints
    constraints ->
                      Usage -> VName -> [PrimType] -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> VName -> [PrimType] -> m ()
    linkVarToTypes Usage
    usage VName
    v [PrimType]
    ts
                StructType
    _ ->
                  Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    Doc ()
    "Cannot instantiate"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "with type"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    tp)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "as"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "must be one of"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "due to"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    old_usage
                      Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        Just (HasFields Liftedness
    l Map Name StructType
    required_fields Usage
    old_usage) -> do
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Liftedness
    l Liftedness -> Liftedness -> Bool
    forall a. Eq a => a -> a -> Bool
    == Liftedness
    Unlifted) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Usage -> BreadCrumbs -> StructType -> m ()
    forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    arrayElemTypeWith Usage
    usage (Usage -> BreadCrumbs
    forall {a}. Pretty a => a -> BreadCrumbs
    unliftedBcs Usage
    old_usage) StructType
    tp
          case StructType
    tp of
            Scalar (Record Map Name StructType
    tp_fields)
              | (Name -> Bool) -> [Name] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Name -> Map Name StructType -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map Name StructType
    tp_fields) ([Name] -> Bool) -> [Name] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Map Name StructType -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name StructType
    required_fields -> do
                  Map Name StructType
    required_fields' <- (StructType -> m StructType)
    -> Map Name StructType -> m (Map Name StructType)
    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) -> Map Name a -> m (Map Name b)
    mapM StructType -> m StructType
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully Map Name StructType
    required_fields
                  let tp' :: StructType
    tp' = ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
    -> ScalarTypeBase Exp NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ Map Name StructType -> ScalarTypeBase Exp NoUniqueness
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record (Map Name StructType -> ScalarTypeBase Exp NoUniqueness)
    -> Map Name StructType -> ScalarTypeBase Exp NoUniqueness
    forall a b. (a -> b) -> a -> b
    $ Map Name StructType
    required_fields Map Name StructType -> Map Name StructType -> Map Name StructType
    forall a. Semigroup a => a -> a -> a
    <> Map Name StructType
    tp_fields -- Crucially left-biased.
                      ext :: [VName]
    ext = (VName -> Bool) -> [VName] -> [VName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` FV -> Set VName
    fvVars (StructType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType StructType
    tp')) [VName]
    bound
                  (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, StructRetType -> Usage -> Constraint
    Constraint ([VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType [VName]
    ext StructType
    tp') Usage
    usage)
                  UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    unifySharedFields UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name StructType
    required_fields' Map Name StructType
    tp_fields
            Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v) []) -> do
              case VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints of
                Just (Int
    _, HasFields Liftedness
    _ Map Name StructType
    tp_fields Usage
    _) ->
                  UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    unifySharedFields UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name StructType
    required_fields Map Name StructType
    tp_fields
                Just (Int
    _, NoConstraint {}) -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                Just (Int
    _, Equality {}) -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                Maybe (Int, Constraint)
    _ -> do
                  Notes
    notes <- Notes -> Notes -> Notes
    forall a. Semigroup a => a -> a -> a
    (<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    vn m (Notes -> Notes) -> m Notes -> m Notes
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    v
                  Notes -> m ()
    forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
    noRecordType Notes
    notes
              m ()
    link
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                ((Int, Constraint) -> (Int, Constraint) -> (Int, Constraint))
    -> VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    M.insertWith
                  (Int, Constraint) -> (Int, Constraint) -> (Int, Constraint)
    forall {a}.
    (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
    combineFields
                  VName
    v
                  (Int
    lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
    HasFields Liftedness
    l Map Name StructType
    required_fields Usage
    old_usage)
              where
                combineFields :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
    combineFields (Int
    _, HasFields Liftedness
    l1 Map Name StructType
    fs1 Usage
    usage1) (a
    _, HasFields Liftedness
    l2 Map Name StructType
    fs2 Usage
    _) =
                  (Int
    lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
    HasFields (Liftedness
    l1 Liftedness -> Liftedness -> Liftedness
    forall a. Ord a => a -> a -> a
    `min` Liftedness
    l2) (Map Name StructType -> Map Name StructType -> Map Name StructType
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    M.union Map Name StructType
    fs1 Map Name StructType
    fs2) Usage
    usage1)
                combineFields (Int, Constraint)
    hasfs (a, Constraint)
    _ = (Int, Constraint)
    hasfs
            StructType
    _ ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Cannot instantiate"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "with type"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    tp)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "as"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "must be a record with fields"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (ScalarTypeBase Exp NoUniqueness -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. ScalarTypeBase Exp NoUniqueness -> Doc ann
    pretty (Map Name StructType -> ScalarTypeBase Exp NoUniqueness
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record Map Name StructType
    required_fields))
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "due to"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    old_usage
                  Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        -- See Note [Linking variables to sum types]
        Just (HasConstrs Liftedness
    l Map Name [StructType]
    required_cs Usage
    old_usage) -> do
          Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    when (Liftedness
    l Liftedness -> Liftedness -> Bool
    forall a. Eq a => a -> a -> Bool
    == Liftedness
    Unlifted) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $ Usage -> BreadCrumbs -> StructType -> m ()
    forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    arrayElemTypeWith Usage
    usage (Usage -> BreadCrumbs
    forall {a}. Pretty a => a -> BreadCrumbs
    unliftedBcs Usage
    old_usage) StructType
    tp
          case StructType
    tp of
            Scalar (Sum Map Name [StructType]
    ts)
              | (Name -> Bool) -> [Name] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Name -> Map Name [StructType] -> Bool
    forall k a. Ord k => k -> Map k a -> Bool
    `M.member` Map Name [StructType]
    ts) ([Name] -> Bool) -> [Name] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Map Name [StructType] -> [Name]
    forall k a. Map k a -> [k]
    M.keys Map Name [StructType]
    required_cs -> do
                  let tp' :: StructType
    tp' = ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
    -> ScalarTypeBase Exp NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
    forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
    Sum (Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness)
    -> Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
    forall a b. (a -> b) -> a -> b
    $ Map Name [StructType]
    required_cs Map Name [StructType]
    -> Map Name [StructType] -> Map Name [StructType]
    forall a. Semigroup a => a -> a -> a
    <> Map Name [StructType]
    ts -- Crucially left-biased.
                      ext :: [VName]
    ext = (VName -> Bool) -> [VName] -> [VName]
    forall a. (a -> Bool) -> [a] -> [a]
    filter (VName -> Set VName -> Bool
    forall a. Ord a => a -> Set a -> Bool
    `S.member` FV -> Set VName
    fvVars (StructType -> FV
    forall u. TypeBase Exp u -> FV
    freeInType StructType
    tp')) [VName]
    bound
                  (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, StructRetType -> Usage -> Constraint
    Constraint ([VName] -> StructType -> StructRetType
    forall dim as. [VName] -> TypeBase dim as -> RetTypeBase dim as
    RetType [VName]
    ext StructType
    tp') Usage
    usage)
                  UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    unifySharedConstructors UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name [StructType]
    required_cs Map Name [StructType]
    ts
              | Bool
    otherwise ->
                  Map Name [StructType] -> Map Name [StructType] -> Notes -> m ()
    forall {m :: * -> *} {t} {a}.
    MonadUnify m =>
    Map Name t -> Map Name t -> Notes -> m a
    unsharedConstructors Map Name [StructType]
    required_cs Map Name [StructType]
    ts (Notes -> m ()) -> m Notes -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    vn
            Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v) []) -> do
              case VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    v Constraints
    constraints of
                Just (Int
    _, HasConstrs Liftedness
    _ Map Name [StructType]
    v_cs Usage
    _) ->
                  UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    unifySharedConstructors UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name [StructType]
    required_cs Map Name [StructType]
    v_cs
                Just (Int
    _, NoConstraint {}) -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                Just (Int
    _, Equality {}) -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
                Maybe (Int, Constraint)
    _ -> do
                  Notes
    notes <- Notes -> Notes -> Notes
    forall a. Semigroup a => a -> a -> a
    (<>) (Notes -> Notes -> Notes) -> m Notes -> m (Notes -> Notes)
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    vn m (Notes -> Notes) -> m Notes -> m Notes
    forall a b. m (a -> b) -> m a -> m b
    forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
    <*> VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    v
                  Notes -> m ()
    forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
    noSumType Notes
    notes
              m ()
    link
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                ((Int, Constraint) -> (Int, Constraint) -> (Int, Constraint))
    -> VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => (a -> a -> a) -> k -> a -> Map k a -> Map k a
    M.insertWith
                  (Int, Constraint) -> (Int, Constraint) -> (Int, Constraint)
    forall {a}.
    (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
    combineConstrs
                  VName
    v
                  (Int
    lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
    HasConstrs Liftedness
    l Map Name [StructType]
    required_cs Usage
    old_usage)
              where
                combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
    combineConstrs (Int
    _, HasConstrs Liftedness
    l1 Map Name [StructType]
    cs1 Usage
    usage1) (a
    _, HasConstrs Liftedness
    l2 Map Name [StructType]
    cs2 Usage
    _) =
                  (Int
    lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
    HasConstrs (Liftedness
    l1 Liftedness -> Liftedness -> Liftedness
    forall a. Ord a => a -> a -> a
    `min` Liftedness
    l2) (Map Name [StructType]
    -> Map Name [StructType] -> Map Name [StructType]
    forall k a. Ord k => Map k a -> Map k a -> Map k a
    M.union Map Name [StructType]
    cs1 Map Name [StructType]
    cs2) Usage
    usage1)
                combineConstrs (Int, Constraint)
    hasCs (a, Constraint)
    _ = (Int, Constraint)
    hasCs
            StructType
    _ -> Notes -> m ()
    forall {m :: * -> *} {a}. MonadUnify m => Notes -> m a
    noSumType (Notes -> m ()) -> m Notes -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< VName -> m Notes
    forall (m :: * -> *). MonadUnify m => VName -> m Notes
    typeVarNotes VName
    vn
        Maybe Constraint
    _ -> m ()
    link
      where
        unsharedConstructors :: Map Name t -> Map Name t -> Notes -> m a
    unsharedConstructors Map Name t
    cs1 Map Name t
    cs2 Notes
    notes =
          Usage -> Notes -> BreadCrumbs -> Doc () -> m a
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError
            Usage
    usage
            Notes
    notes
            BreadCrumbs
    bcs
            (Map Name t -> Map Name t -> Doc ()
    forall t a. Map Name t -> Map Name t -> Doc a
    unsharedConstructorsMsg Map Name t
    cs1 Map Name t
    cs2)
        noSumType :: Notes -> m a
    noSumType Notes
    notes =
          Usage -> Notes -> BreadCrumbs -> Doc () -> m a
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError
            Usage
    usage
            Notes
    notes
            BreadCrumbs
    bcs
            Doc ()
    "Cannot unify a sum type with a non-sum type."
        noRecordType :: Notes -> m a
    noRecordType Notes
    notes =
          Usage -> Notes -> BreadCrumbs -> Doc () -> m a
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError
            Usage
    usage
            Notes
    notes
            BreadCrumbs
    bcs
            Doc ()
    "Cannot unify a record type with a non-record type."

    linkVarToDim ::
      (MonadUnify m) =>
      Usage ->
      BreadCrumbs ->
      VName ->
      Level ->
      Exp ->
      m ()
    linkVarToDim :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> Exp -> m ()
    linkVarToDim Usage
    usage BreadCrumbs
    bcs VName
    vn Int
    lvl Exp
    e = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints

      (VName -> m ()) -> Set VName -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Constraints -> VName -> m ()
    forall {m :: * -> *}. MonadUnify m => Constraints -> VName -> m ()
    checkVar Constraints
    constraints) (Set VName -> m ()) -> Set VName -> m ()
    forall a b. (a -> b) -> a -> b
    $ FV -> Set VName
    fvVars (FV -> Set VName) -> FV -> Set VName
    forall a b. (a -> b) -> a -> b
    $ Exp -> FV
    freeInExp Exp
    e

      (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Maybe Exp -> Usage -> Constraint
    Size (Exp -> Maybe Exp
    forall a. a -> Maybe a
    Just Exp
    e) Usage
    usage)
      where
        checkVar :: Constraints -> VName -> m ()
    checkVar Constraints
    _ VName
    dim'
          | VName
    vn VName -> VName -> Bool
    forall a. Eq a => a -> a -> Bool
    == VName
    dim' = do
              Notes
    notes <- Usage -> Exp -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes Usage
    usage Exp
    e
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    notes BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Occurs check: cannot instantiate"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "with"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Exp -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Exp -> Doc ann
    pretty Exp
    e)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "."
        checkVar Constraints
    constraints VName
    dim'
          | Just (Int
    dim_lvl, Constraint
    c) <- VName
    dim' VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    `M.lookup` Constraints
    constraints,
            Int
    dim_lvl Int -> Int -> Bool
    forall a. Ord a => a -> a -> Bool
    >= Int
    lvl =
              case Constraint
    c of
                ParamSize {} -> do
                  Notes
    notes <- Usage -> Exp -> m Notes
    forall a (m :: * -> *).
    (Located a, MonadUnify m) =>
    a -> Exp -> m Notes
    dimNotes Usage
    usage Exp
    e
                  Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    notes BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    Doc ()
    "Cannot link size"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "to"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Exp -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Exp -> Doc ann
    pretty Exp
    e)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "(scope violation)."
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "This is because"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (QualName VName -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. QualName VName -> Doc ann
    pretty (QualName VName -> Doc ()) -> QualName VName -> Doc ()
    forall a b. (a -> b) -> a -> b
    $ VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    dim')
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "is not in scope when"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "is introduced."
                Constraint
    _ -> (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    dim' (Int
    lvl, Constraint
    c)
        checkVar Constraints
    _ VName
    _ = () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    -- | Assert that this type must be one of the given primitive types.
    mustBeOneOf :: (MonadUnify m) => [PrimType] -> Usage -> StructType -> m ()
    mustBeOneOf :: forall (m :: * -> *).
    MonadUnify m =>
    [PrimType] -> Usage -> StructType -> m ()
    mustBeOneOf [PrimType
    req_t] Usage
    usage StructType
    t = Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage (ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (PrimType -> ScalarTypeBase Exp NoUniqueness
    forall dim u. PrimType -> ScalarTypeBase dim u
    Prim PrimType
    req_t)) StructType
    t
    mustBeOneOf [PrimType]
    ts Usage
    usage StructType
    t = do
      StructType
    t' <- StructType -> m StructType
    forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType StructType
    t
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      let isRigid' :: VName -> Bool
    isRigid' VName
    v = VName -> Constraints -> Bool
    isRigid VName
    v Constraints
    constraints

      case StructType
    t' of
        Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    v) [])
          | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ VName -> Bool
    isRigid' VName
    v -> Usage -> VName -> [PrimType] -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> VName -> [PrimType] -> m ()
    linkVarToTypes Usage
    usage VName
    v [PrimType]
    ts
        Scalar (Prim PrimType
    pt) | PrimType
    pt PrimType -> [PrimType] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [PrimType]
    ts -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
        StructType
    _ -> m ()
    forall {a}. m a
    failure
      where
        failure :: m a
    failure =
          Usage -> Notes -> BreadCrumbs -> Doc () -> m a
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m a) -> Doc () -> m a
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Cannot unify type"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t)
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "with any of "
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."

    linkVarToTypes :: (MonadUnify m) => Usage -> VName -> [PrimType] -> m ()
    linkVarToTypes :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> VName -> [PrimType] -> m ()
    linkVarToTypes Usage
    usage VName
    vn [PrimType]
    ts = do
      Maybe (Int, Constraint)
    vn_constraint <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    vn (Constraints -> Maybe (Int, Constraint))
    -> m Constraints -> m (Maybe (Int, Constraint))
    forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
    <$> m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      case Maybe (Int, Constraint)
    vn_constraint of
        Just (Int
    lvl, Overloaded [PrimType]
    vn_ts Usage
    vn_usage) ->
          case [PrimType]
    ts [PrimType] -> [PrimType] -> [PrimType]
    forall a. Eq a => [a] -> [a] -> [a]
    `L.intersect` [PrimType]
    vn_ts of
            [] ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Type constrained to one of"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "but also one of"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    vn_ts)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "due to"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    vn_usage
                  Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
            [PrimType]
    ts' -> (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, [PrimType] -> Usage -> Constraint
    Overloaded [PrimType]
    ts' Usage
    usage)
        Just (Int
    _, HasConstrs Liftedness
    _ Map Name [StructType]
    _ Usage
    vn_usage) ->
          Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Type constrained to one of"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    ", but also inferred to be sum type due to"
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    vn_usage
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        Just (Int
    _, HasFields Liftedness
    _ Map Name StructType
    _ Usage
    vn_usage) ->
          Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Type constrained to one of"
              Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    ", but also inferred to be record due to"
                Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    vn_usage
              Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        Just (Int
    lvl, Constraint
    _) -> (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, [PrimType] -> Usage -> Constraint
    Overloaded [PrimType]
    ts Usage
    usage)
        Maybe (Int, Constraint)
    Nothing ->
          Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
            Doc ()
    "Cannot constrain type to one of" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> [Doc ()] -> Doc ()
    forall a. [Doc a] -> Doc a
    commasep ((PrimType -> Doc ()) -> [PrimType] -> [Doc ()]
    forall a b. (a -> b) -> [a] -> [b]
    map PrimType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. PrimType -> Doc ann
    pretty [PrimType]
    ts)

    -- | Assert that this type must support equality.
    equalityType ::
      (MonadUnify m, Pretty (Shape dim), Pretty u) =>
      Usage ->
      TypeBase dim u ->
      m ()
    equalityType :: forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> TypeBase dim u -> m ()
    equalityType Usage
    usage TypeBase dim u
    t = do
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (TypeBase dim u -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero TypeBase dim u
    t) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
          Doc ()
    "Type " Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (TypeBase dim u -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase dim u -> Doc ann
    pretty TypeBase dim u
    t) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "does not support equality (may contain function)."
      (VName -> m ()) -> Set VName -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ VName -> m ()
    forall {m :: * -> *}. MonadUnify m => VName -> m ()
    mustBeEquality (Set VName -> m ()) -> Set VName -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeBase dim u -> Set VName
    forall dim as. TypeBase dim as -> Set VName
    typeVars TypeBase dim u
    t
      where
        mustBeEquality :: VName -> m ()
    mustBeEquality VName
    vn = do
          Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
          case VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    vn Constraints
    constraints of
            Just (Int
    _, Constraint (RetType [] (Scalar (TypeVar NoUniqueness
    _ (QualName [] VName
    vn') []))) Usage
    _) ->
              VName -> m ()
    mustBeEquality VName
    vn'
            Just (Int
    _, Constraint (RetType [VName]
    _ StructType
    vn_t) Usage
    cusage)
              | Bool -> Bool
    not (Bool -> Bool) -> Bool -> Bool
    forall a b. (a -> b) -> a -> b
    $ StructType -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero StructType
    vn_t ->
                  Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    Doc ()
    "Type"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (TypeBase dim u -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase dim u -> Doc ann
    pretty TypeBase dim u
    t)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "does not support equality."
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "Constrained to be higher-order due to"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Usage -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Usage -> Doc ann
    pretty Usage
    cusage
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "."
              | Bool
    otherwise -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            Just (Int
    lvl, NoConstraint Liftedness
    _ Usage
    _) ->
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Usage -> Constraint
    Equality Usage
    usage)
            Just (Int
    _, Overloaded [PrimType]
    _ Usage
    _) ->
              () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure () -- All primtypes support equality.
            Just (Int
    _, Equality {}) ->
              () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
            Maybe (Int, Constraint)
    _ ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Type" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "does not support equality."

    zeroOrderTypeWith ::
      (MonadUnify m) =>
      Usage ->
      BreadCrumbs ->
      StructType ->
      m ()
    zeroOrderTypeWith :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> StructType -> m ()
    zeroOrderTypeWith Usage
    usage BreadCrumbs
    bcs StructType
    t = do
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (StructType -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero StructType
    t) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
          Doc ()
    "Type" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "found to be functional."
      (VName -> m ()) -> [VName] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ VName -> m ()
    forall {m :: * -> *}. MonadUnify m => VName -> m ()
    mustBeZeroOrder ([VName] -> m ()) -> (StructType -> [VName]) -> StructType -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set VName -> [VName]
    forall a. Set a -> [a]
    S.toList (Set VName -> [VName])
    -> (StructType -> Set VName) -> StructType -> [VName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . StructType -> Set VName
    forall dim as. TypeBase dim as -> Set VName
    typeVars (StructType -> m ()) -> m StructType -> m ()
    forall (m :: * -> *) a b. Monad m => (a -> m b) -> m a -> m b
    =<< StructType -> m StructType
    forall (m :: * -> *). MonadUnify m => StructType -> m StructType
    normType StructType
    t
      where
        mustBeZeroOrder :: VName -> m ()
    mustBeZeroOrder VName
    vn = do
          Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
          case VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    vn Constraints
    constraints of
            Just (Int
    lvl, NoConstraint Liftedness
    _ Usage
    _) ->
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Liftedness -> Usage -> Constraint
    NoConstraint Liftedness
    Unlifted Usage
    usage)
            Just (Int
    lvl, HasFields Liftedness
    _ Map Name StructType
    fs Usage
    _) ->
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
    HasFields Liftedness
    Unlifted Map Name StructType
    fs Usage
    usage)
            Just (Int
    lvl, HasConstrs Liftedness
    _ Map Name [StructType]
    cs Usage
    _) ->
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
    HasConstrs Liftedness
    Unlifted Map Name [StructType]
    cs Usage
    usage)
            Just (Int
    _, ParamType Liftedness
    Lifted Loc
    ploc) ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Type parameter"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "at"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> String
    forall a. Located a => a -> String
    locStr Loc
    ploc)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "may be a function."
            Maybe (Int, Constraint)
    _ -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    -- | Assert that this type must be zero-order.
    zeroOrderType ::
      (MonadUnify m) => Usage -> T.Text -> StructType -> m ()
    zeroOrderType :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> Text -> StructType -> m ()
    zeroOrderType Usage
    usage Text
    desc =
      Usage -> BreadCrumbs -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> StructType -> m ()
    zeroOrderTypeWith Usage
    usage (BreadCrumbs -> StructType -> m ())
    -> BreadCrumbs -> StructType -> m ()
    forall a b. (a -> b) -> a -> b
    $ BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb BreadCrumb
    bc BreadCrumbs
    noBreadCrumbs
      where
        bc :: BreadCrumb
    bc = Doc () -> BreadCrumb
    Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
    forall a b. (a -> b) -> a -> b
    $ Doc ()
    "When checking" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Text -> Doc ()
    forall a. Text -> Doc a
    textwrap Text
    desc

    arrayElemTypeWith ::
      (MonadUnify m, Pretty (Shape dim), Pretty u) =>
      Usage ->
      BreadCrumbs ->
      TypeBase dim u ->
      m ()
    arrayElemTypeWith :: forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    arrayElemTypeWith Usage
    usage BreadCrumbs
    bcs TypeBase dim u
    t = do
      Bool -> m () -> m ()
    forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
    unless (TypeBase dim u -> Bool
    forall dim as. TypeBase dim as -> Bool
    orderZero TypeBase dim u
    t) (m () -> m ()) -> m () -> m ()
    forall a b. (a -> b) -> a -> b
    $
        Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
          Doc ()
    "Type" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc () -> Doc ()
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (TypeBase dim u -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase dim u -> Doc ann
    pretty TypeBase dim u
    t) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    </> Doc ()
    "found to be functional."
      (VName -> m ()) -> [VName] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ VName -> m ()
    forall {m :: * -> *}. MonadUnify m => VName -> m ()
    mustBeZeroOrder ([VName] -> m ())
    -> (TypeBase dim u -> [VName]) -> TypeBase dim u -> m ()
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . Set VName -> [VName]
    forall a. Set a -> [a]
    S.toList (Set VName -> [VName])
    -> (TypeBase dim u -> Set VName) -> TypeBase dim u -> [VName]
    forall b c a. (b -> c) -> (a -> b) -> a -> c
    . TypeBase dim u -> Set VName
    forall dim as. TypeBase dim as -> Set VName
    typeVars (TypeBase dim u -> m ()) -> TypeBase dim u -> m ()
    forall a b. (a -> b) -> a -> b
    $ TypeBase dim u
    t
      where
        mustBeZeroOrder :: VName -> m ()
    mustBeZeroOrder VName
    vn = do
          Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
          case VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    vn Constraints
    constraints of
            Just (Int
    lvl, NoConstraint Liftedness
    _ Usage
    _) ->
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    vn (Int
    lvl, Liftedness -> Usage -> Constraint
    NoConstraint Liftedness
    Unlifted Usage
    usage)
            Just (Int
    _, ParamType Liftedness
    l Loc
    ploc)
              | Liftedness
    l Liftedness -> [Liftedness] -> Bool
    forall a. Eq a => a -> [a] -> Bool
    forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
    `elem` [Liftedness
    Lifted, Liftedness
    SizeLifted] ->
                  Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    Doc ()
    "Type parameter"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (VName -> Doc ()
    forall a. VName -> Doc a
    forall v a. IsName v => v -> Doc a
    prettyName VName
    vn)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "bound at"
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> String -> Doc ()
    forall ann. String -> Doc ann
    forall a ann. Pretty a => a -> Doc ann
    pretty (Loc -> String
    forall a. Located a => a -> String
    locStr Loc
    ploc)
                      Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "is lifted and cannot be an array element."
            Maybe (Int, Constraint)
    _ -> () -> m ()
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()

    -- | Assert that this type must be valid as an array element.
    arrayElemType ::
      (MonadUnify m, Pretty (Shape dim), Pretty u) =>
      Usage ->
      T.Text ->
      TypeBase dim u ->
      m ()
    arrayElemType :: forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> Text -> TypeBase dim u -> m ()
    arrayElemType Usage
    usage Text
    desc =
      Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    forall (m :: * -> *) dim u.
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage -> BreadCrumbs -> TypeBase dim u -> m ()
    arrayElemTypeWith Usage
    usage (BreadCrumbs -> TypeBase dim u -> m ())
    -> BreadCrumbs -> TypeBase dim u -> m ()
    forall a b. (a -> b) -> a -> b
    $ BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb BreadCrumb
    bc BreadCrumbs
    noBreadCrumbs
      where
        bc :: BreadCrumb
    bc = Doc () -> BreadCrumb
    Matching (Doc () -> BreadCrumb) -> Doc () -> BreadCrumb
    forall a b. (a -> b) -> a -> b
    $ Doc ()
    "When checking" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Text -> Doc ()
    forall a. Text -> Doc a
    textwrap Text
    desc

    unifySharedFields ::
      (MonadUnify m) =>
      UnifySizes m ->
      Usage ->
      [VName] ->
      BreadCrumbs ->
      M.Map Name StructType ->
      M.Map Name StructType ->
      m ()
    unifySharedFields :: forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name StructType
    -> Map Name StructType
    -> m ()
    unifySharedFields UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name StructType
    fs1 Map Name StructType
    fs2 =
      [(Name, (StructType, StructType))]
    -> ((Name, (StructType, StructType)) -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (Map Name (StructType, StructType)
    -> [(Name, (StructType, StructType))]
    forall k a. Map k a -> [(k, a)]
    M.toList (Map Name (StructType, StructType)
     -> [(Name, (StructType, StructType))])
    -> Map Name (StructType, StructType)
    -> [(Name, (StructType, StructType))]
    forall a b. (a -> b) -> a -> b
    $ (StructType -> StructType -> (StructType, StructType))
    -> Map Name StructType
    -> Map Name StructType
    -> Map Name (StructType, StructType)
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    M.intersectionWith (,) Map Name StructType
    fs1 Map Name StructType
    fs2) (((Name, (StructType, StructType)) -> m ()) -> m ())
    -> ((Name, (StructType, StructType)) -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \(Name
    f, (StructType
    t1, StructType
    t2)) ->
        UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith UnifySizes m
    onDims Usage
    usage [VName]
    bound (BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb ([Name] -> BreadCrumb
    MatchingFields [Name
    f]) BreadCrumbs
    bcs) StructType
    t1 StructType
    t2

    unifySharedConstructors ::
      (MonadUnify m) =>
      UnifySizes m ->
      Usage ->
      [VName] ->
      BreadCrumbs ->
      M.Map Name [StructType] ->
      M.Map Name [StructType] ->
      m ()
    unifySharedConstructors :: forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> m ()
    unifySharedConstructors UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Map Name [StructType]
    cs1 Map Name [StructType]
    cs2 =
      [(Name, ([StructType], [StructType]))]
    -> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    t a -> (a -> m b) -> m ()
    forM_ (Map Name ([StructType], [StructType])
    -> [(Name, ([StructType], [StructType]))]
    forall k a. Map k a -> [(k, a)]
    M.toList (Map Name ([StructType], [StructType])
     -> [(Name, ([StructType], [StructType]))])
    -> Map Name ([StructType], [StructType])
    -> [(Name, ([StructType], [StructType]))]
    forall a b. (a -> b) -> a -> b
    $ ([StructType] -> [StructType] -> ([StructType], [StructType]))
    -> Map Name [StructType]
    -> Map Name [StructType]
    -> Map Name ([StructType], [StructType])
    forall k a b c.
    Ord k =>
    (a -> b -> c) -> Map k a -> Map k b -> Map k c
    M.intersectionWith (,) Map Name [StructType]
    cs1 Map Name [StructType]
    cs2) (((Name, ([StructType], [StructType])) -> m ()) -> m ())
    -> ((Name, ([StructType], [StructType])) -> m ()) -> m ()
    forall a b. (a -> b) -> a -> b
    $ \(Name
    c, ([StructType]
    f1, [StructType]
    f2)) ->
        Name -> [StructType] -> [StructType] -> m ()
    unifyConstructor Name
    c [StructType]
    f1 [StructType]
    f2
      where
        unifyConstructor :: Name -> [StructType] -> [StructType] -> m ()
    unifyConstructor Name
    c [StructType]
    f1 [StructType]
    f2
          | [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    f1 Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    f2 = do
              let bcs' :: BreadCrumbs
    bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
    breadCrumb (Name -> BreadCrumb
    MatchingConstructor Name
    c) BreadCrumbs
    bcs
              (StructType -> StructType -> m ())
    -> [StructType] -> [StructType] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs') [StructType]
    f1 [StructType]
    f2
          | Bool
    otherwise =
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Cannot unify constructor" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall ann. Name -> Doc ann
    forall v a. IsName v => v -> Doc a
    prettyName Name
    c) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."

    -- | In @mustHaveConstr usage c t fs@, the type @t@ must have a
    -- constructor named @c@ that takes arguments of types @ts@.
    mustHaveConstr ::
      (MonadUnify m) =>
      Usage ->
      Name ->
      StructType ->
      [StructType] ->
      m ()
    mustHaveConstr :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> Name -> StructType -> [StructType] -> m ()
    mustHaveConstr Usage
    usage Name
    c StructType
    t [StructType]
    fs = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      case StructType
    t of
        Scalar (TypeVar NoUniqueness
    _ (QualName [VName]
    _ VName
    tn) [])
          | Just (Int
    lvl, NoConstraint Liftedness
    l Usage
    _) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    tn Constraints
    constraints -> do
              (StructType -> m ()) -> [StructType] -> m ()
    forall (t :: * -> *) (m :: * -> *) a b.
    (Foldable t, Monad m) =>
    (a -> m b) -> t a -> m ()
    mapM_ (Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    scopeCheck Usage
    usage BreadCrumbs
    noBreadCrumbs VName
    tn Int
    lvl) [StructType]
    fs
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    tn (Int
    lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
    HasConstrs Liftedness
    l (Name -> [StructType] -> Map Name [StructType]
    forall k a. k -> a -> Map k a
    M.singleton Name
    c [StructType]
    fs) Usage
    usage)
          | Just (Int
    lvl, HasConstrs Liftedness
    l Map Name [StructType]
    cs Usage
    _) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    tn Constraints
    constraints ->
              case Name -> Map Name [StructType] -> Maybe [StructType]
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Name
    c Map Name [StructType]
    cs of
                Maybe [StructType]
    Nothing ->
                  (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    tn (Int
    lvl, Liftedness -> Map Name [StructType] -> Usage -> Constraint
    HasConstrs Liftedness
    l (Name
    -> [StructType] -> Map Name [StructType] -> Map Name [StructType]
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert Name
    c [StructType]
    fs Map Name [StructType]
    cs) Usage
    usage)
                Just [StructType]
    fs'
                  | [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    fs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    fs' -> (StructType -> StructType -> m ())
    -> [StructType] -> [StructType] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage) [StructType]
    fs [StructType]
    fs'
                  | Bool
    otherwise ->
                      Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                        Doc ()
    "Different arity for constructor" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty Name
    c) Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        Scalar (Sum Map Name [StructType]
    cs) ->
          case Name -> Map Name [StructType] -> Maybe [StructType]
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Name
    c Map Name [StructType]
    cs of
            Maybe [StructType]
    Nothing ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Constuctor" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty Name
    c) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "not present in type."
            Just [StructType]
    fs'
              | [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    fs Int -> Int -> Bool
    forall a. Eq a => a -> a -> Bool
    == [StructType] -> Int
    forall a. [a] -> Int
    forall (t :: * -> *) a. Foldable t => t a -> Int
    length [StructType]
    fs' -> (StructType -> StructType -> m ())
    -> [StructType] -> [StructType] -> m ()
    forall (m :: * -> *) a b c.
    Applicative m =>
    (a -> b -> m c) -> [a] -> [b] -> m ()
    zipWithM_ (Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage) [StructType]
    fs [StructType]
    fs'
              | Bool
    otherwise ->
                  Usage -> Notes -> BreadCrumbs -> Doc () -> m ()
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs (Doc () -> m ()) -> Doc () -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    Doc ()
    "Different arity for constructor" Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty Name
    c) Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    "."
        StructType
    _ ->
          Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage StructType
    t (StructType -> m ()) -> StructType -> m ()
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
    -> ScalarTypeBase Exp NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
    forall dim u. Map Name [TypeBase dim u] -> ScalarTypeBase dim u
    Sum (Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness)
    -> Map Name [StructType] -> ScalarTypeBase Exp NoUniqueness
    forall a b. (a -> b) -> a -> b
    $ Name -> [StructType] -> Map Name [StructType]
    forall k a. k -> a -> Map k a
    M.singleton Name
    c [StructType]
    fs

    mustHaveFieldWith ::
      (MonadUnify m) =>
      UnifySizes m ->
      Usage ->
      [VName] ->
      BreadCrumbs ->
      Name ->
      StructType ->
      m StructType
    mustHaveFieldWith :: forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Name
    -> StructType
    -> m StructType
    mustHaveFieldWith UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs Name
    l StructType
    t = do
      Constraints
    constraints <- m Constraints
    forall (m :: * -> *). MonadUnify m => m Constraints
    getConstraints
      StructType
    l_type <- Loc -> Name -> m StructType
    forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    forall (m :: * -> *) als a dim.
    (MonadUnify m, Monoid als, Located a) =>
    a -> Name -> m (TypeBase dim als)
    newTypeVar (Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage) Name
    "t"
      case StructType
    t of
        Scalar (TypeVar NoUniqueness
    _ (QualName [VName]
    _ VName
    tn) [])
          | Just (Int
    lvl, NoConstraint {}) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    tn Constraints
    constraints -> do
              Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> BreadCrumbs -> VName -> Int -> StructType -> m ()
    scopeCheck Usage
    usage BreadCrumbs
    bcs VName
    tn Int
    lvl StructType
    l_type
              (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    tn (Int
    lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
    HasFields Liftedness
    Lifted (Name -> StructType -> Map Name StructType
    forall k a. k -> a -> Map k a
    M.singleton Name
    l StructType
    l_type) Usage
    usage)
              StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    l_type
          | Just (Int
    lvl, HasFields Liftedness
    lifted Map Name StructType
    fields Usage
    _) <- VName -> Constraints -> Maybe (Int, Constraint)
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup VName
    tn Constraints
    constraints -> do
              case Name -> Map Name StructType -> Maybe StructType
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Name
    l Map Name StructType
    fields of
                Just StructType
    t' -> UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith UnifySizes m
    onDims Usage
    usage [VName]
    bound BreadCrumbs
    bcs StructType
    l_type StructType
    t'
                Maybe StructType
    Nothing ->
                  (Constraints -> Constraints) -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> m ())
    -> (Constraints -> Constraints) -> m ()
    forall a b. (a -> b) -> a -> b
    $
                    VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert
                      VName
    tn
                      (Int
    lvl, Liftedness -> Map Name StructType -> Usage -> Constraint
    HasFields Liftedness
    lifted (Name -> StructType -> Map Name StructType -> Map Name StructType
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert Name
    l StructType
    l_type Map Name StructType
    fields) Usage
    usage)
              StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    l_type
        Scalar (Record Map Name StructType
    fields)
          | Just StructType
    t' <- Name -> Map Name StructType -> Maybe StructType
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup Name
    l Map Name StructType
    fields -> do
              Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage StructType
    l_type StructType
    t'
              StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    t'
          | Bool
    otherwise ->
              Usage -> Notes -> BreadCrumbs -> Doc () -> m StructType
    forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    forall (m :: * -> *) loc a.
    (MonadUnify m, Located loc) =>
    loc -> Notes -> BreadCrumbs -> Doc () -> m a
    unifyError Usage
    usage Notes
    forall a. Monoid a => a
    mempty BreadCrumbs
    bcs (Doc () -> m StructType) -> Doc () -> m StructType
    forall a b. (a -> b) -> a -> b
    $
                Doc ()
    "Attempt to access field"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc () -> Doc ()
    forall ann. Doc ann -> Doc ann
    dquotes (Name -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. Name -> Doc ann
    pretty Name
    l)
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> Doc ()
    " of value of type"
                  Doc () -> Doc () -> Doc ()
    forall a. Doc a -> Doc a -> Doc a
    <+> TypeBase () () -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. TypeBase () () -> Doc ann
    pretty (StructType -> TypeBase () ()
    forall dim as. TypeBase dim as -> TypeBase () ()
    toStructural StructType
    t)
                  Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> Doc ()
    "."
        StructType
    _ -> do
          Usage -> StructType -> StructType -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify Usage
    usage StructType
    t (StructType -> m ()) -> StructType -> m ()
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase Exp NoUniqueness -> StructType
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase Exp NoUniqueness -> StructType)
    -> ScalarTypeBase Exp NoUniqueness -> StructType
    forall a b. (a -> b) -> a -> b
    $ Map Name StructType -> ScalarTypeBase Exp NoUniqueness
    forall dim u. Map Name (TypeBase dim u) -> ScalarTypeBase dim u
    Record (Map Name StructType -> ScalarTypeBase Exp NoUniqueness)
    -> Map Name StructType -> ScalarTypeBase Exp NoUniqueness
    forall a b. (a -> b) -> a -> b
    $ Name -> StructType -> Map Name StructType
    forall k a. k -> a -> Map k a
    M.singleton Name
    l StructType
    l_type
          StructType -> m StructType
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure StructType
    l_type

    -- | Assert that some type must have a field with this name and type.
    mustHaveField ::
      (MonadUnify m) =>
      Usage ->
      Name ->
      StructType ->
      m StructType
    mustHaveField :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> Name -> StructType -> m StructType
    mustHaveField Usage
    usage = UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Name
    -> StructType
    -> m StructType
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> Name
    -> StructType
    -> m StructType
    mustHaveFieldWith (Usage -> UnifySizes m
    forall (m :: * -> *). MonadUnify m => Usage -> UnifySizes m
    unifySizes Usage
    usage) Usage
    usage [VName]
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs

    newDimOnMismatch ::
      (MonadUnify m) =>
      Loc ->
      StructType ->
      StructType ->
      m (StructType, [VName])
    newDimOnMismatch :: forall (m :: * -> *).
    MonadUnify m =>
    Loc -> StructType -> StructType -> m (StructType, [VName])
    newDimOnMismatch Loc
    loc StructType
    t1 StructType
    t2 = do
      (StructType
    t, Map (Exp, Exp) VName
    seen) <- StateT (Map (Exp, Exp) VName) m StructType
    -> Map (Exp, Exp) VName -> m (StructType, Map (Exp, Exp) VName)
    forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
    runStateT (([VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp)
    -> StructType
    -> StructType
    -> StateT (Map (Exp, Exp) VName) m StructType
    forall as (m :: * -> *) d1 d2.
    (Monoid as, Monad m) =>
    ([VName] -> d1 -> d2 -> m d1)
    -> TypeBase d1 as -> TypeBase d2 as -> m (TypeBase d1 as)
    matchDims [VName] -> Exp -> Exp -> StateT (Map (Exp, Exp) VName) m Exp
    forall {t :: (* -> *) -> * -> *} {m :: * -> *} {p}.
    (MonadState (Map (Exp, Exp) VName) (t m), MonadTrans t,
     MonadUnify m) =>
    p -> Exp -> Exp -> t m Exp
    onDims StructType
    t1 StructType
    t2) Map (Exp, Exp) VName
    forall a. Monoid a => a
    mempty
      (StructType, [VName]) -> m (StructType, [VName])
    forall a. a -> m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (StructType
    t, Map (Exp, Exp) VName -> [VName]
    forall k a. Map k a -> [a]
    M.elems Map (Exp, Exp) VName
    seen)
      where
        r :: RigidSource
    r = StructType -> StructType -> RigidSource
    RigidCond StructType
    t1 StructType
    t2
        same :: (Exp, Exp) -> Bool
    same (Exp
    e1, Exp
    e2) =
          Bool -> ([(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
    forall b a. b -> (a -> b) -> Maybe a -> b
    maybe Bool
    False (((Exp, Exp) -> Bool) -> [(Exp, Exp)] -> Bool
    forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
    all (Exp, Exp) -> Bool
    same) (Maybe [(Exp, Exp)] -> Bool) -> Maybe [(Exp, Exp)] -> Bool
    forall a b. (a -> b) -> a -> b
    $ Exp -> Exp -> Maybe [(Exp, Exp)]
    similarExps Exp
    e1 Exp
    e2
        onDims :: p -> Exp -> Exp -> t m Exp
    onDims p
    _ Exp
    d1 Exp
    d2
          | (Exp, Exp) -> Bool
    same (Exp
    d1, Exp
    d2) = Exp -> t m Exp
    forall a. a -> t m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Exp
    d1
          | Bool
    otherwise = do
              -- Remember mismatches we have seen before and reuse the
              -- same new size.
              Maybe VName
    maybe_d <- (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets ((Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName))
    -> (Map (Exp, Exp) VName -> Maybe VName) -> t m (Maybe VName)
    forall a b. (a -> b) -> a -> b
    $ (Exp, Exp) -> Map (Exp, Exp) VName -> Maybe VName
    forall k a. Ord k => k -> Map k a -> Maybe a
    M.lookup (Exp
    d1, Exp
    d2)
              case Maybe VName
    maybe_d of
                Just VName
    d -> Exp -> t m Exp
    forall a. a -> t m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Exp -> t m Exp) -> Exp -> t m Exp
    forall a b. (a -> b) -> a -> b
    $ QualName VName -> SrcLoc -> Exp
    sizeFromName (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    d) (SrcLoc -> Exp) -> SrcLoc -> Exp
    forall a b. (a -> b) -> a -> b
    $ Loc -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf Loc
    loc
                Maybe VName
    Nothing -> do
                  VName
    d <- m VName -> t m VName
    forall (m :: * -> *) a. Monad m => m a -> t m a
    forall (t :: (* -> *) -> * -> *) (m :: * -> *) a.
    (MonadTrans t, Monad m) =>
    m a -> t m a
    lift (m VName -> t m VName) -> m VName -> t m VName
    forall a b. (a -> b) -> a -> b
    $ Loc -> RigidSource -> Name -> m VName
    forall a. Located a => a -> RigidSource -> Name -> m VName
    forall (m :: * -> *) a.
    (MonadUnify m, Located a) =>
    a -> RigidSource -> Name -> m VName
    newRigidDim Loc
    loc RigidSource
    r Name
    "differ"
                  (Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify ((Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ())
    -> (Map (Exp, Exp) VName -> Map (Exp, Exp) VName) -> t m ()
    forall a b. (a -> b) -> a -> b
    $ (Exp, Exp) -> VName -> Map (Exp, Exp) VName -> Map (Exp, Exp) VName
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert (Exp
    d1, Exp
    d2) VName
    d
                  Exp -> t m Exp
    forall a. a -> t m a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (Exp -> t m Exp) -> Exp -> t m Exp
    forall a b. (a -> b) -> a -> b
    $ QualName VName -> SrcLoc -> Exp
    sizeFromName (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    d) (SrcLoc -> Exp) -> SrcLoc -> Exp
    forall a b. (a -> b) -> a -> b
    $ Loc -> SrcLoc
    forall a. Located a => a -> SrcLoc
    srclocOf Loc
    loc

    -- | Like unification, but creates new size variables where mismatches
    -- occur.  Returns the new dimensions thus created.
    unifyMostCommon ::
      (MonadUnify m) =>
      Usage ->
      StructType ->
      StructType ->
      m (StructType, [VName])
    unifyMostCommon :: forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m (StructType, [VName])
    unifyMostCommon Usage
    usage StructType
    t1 StructType
    t2 = do
      -- We are ignoring the dimensions here, because any mismatches
      -- should be turned into fresh size variables.
      let allOK :: p -> p -> p -> p -> p -> f ()
    allOK p
    _ p
    _ p
    _ p
    _ p
    _ = () -> f ()
    forall a. a -> f a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure ()
      UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    forall (m :: * -> *).
    MonadUnify m =>
    UnifySizes m
    -> Usage
    -> [VName]
    -> BreadCrumbs
    -> StructType
    -> StructType
    -> m ()
    unifyWith UnifySizes m
    forall {f :: * -> *} {p} {p} {p} {p} {p}.
    Applicative f =>
    p -> p -> p -> p -> p -> f ()
    allOK Usage
    usage [VName]
    forall a. Monoid a => a
    mempty BreadCrumbs
    noBreadCrumbs StructType
    t1 StructType
    t2
      StructType
    t1' <- StructType -> m StructType
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully StructType
    t1
      StructType
    t2' <- StructType -> m StructType
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully StructType
    t2
      Loc -> StructType -> StructType -> m (StructType, [VName])
    forall (m :: * -> *).
    MonadUnify m =>
    Loc -> StructType -> StructType -> m (StructType, [VName])
    newDimOnMismatch (Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage) StructType
    t1' StructType
    t2'

    -- Simple MonadUnify implementation.

    type UnifyMState = (Constraints, Int)

    newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
      deriving
        ( Applicative UnifyM
    Applicative UnifyM =>
    (forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b)
    -> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
    -> (forall a. a -> UnifyM a)
    -> Monad UnifyM
    forall a. a -> UnifyM a
    forall a b. UnifyM a -> UnifyM b -> UnifyM b
    forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
    forall (m :: * -> *).
    Applicative m =>
    (forall a b. m a -> (a -> m b) -> m b)
    -> (forall a b. m a -> m b -> m b)
    -> (forall a. a -> m a)
    -> Monad m
    $c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
    >>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
    $c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
    >> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
    $creturn :: forall a. a -> UnifyM a
    return :: forall a. a -> UnifyM a
    Monad,
          (forall a b. (a -> b) -> UnifyM a -> UnifyM b)
    -> (forall a b. a -> UnifyM b -> UnifyM a) -> Functor UnifyM
    forall a b. a -> UnifyM b -> UnifyM a
    forall a b. (a -> b) -> UnifyM a -> UnifyM b
    forall (f :: * -> *).
    (forall a b. (a -> b) -> f a -> f b)
    -> (forall a b. a -> f b -> f a) -> Functor f
    $cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
    fmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
    $c<$ :: forall a b. a -> UnifyM b -> UnifyM a
    <$ :: forall a b. a -> UnifyM b -> UnifyM a
    Functor,
          Functor UnifyM
    Functor UnifyM =>
    (forall a. a -> UnifyM a)
    -> (forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b)
    -> (forall a b c.
        (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c)
    -> (forall a b. UnifyM a -> UnifyM b -> UnifyM b)
    -> (forall a b. UnifyM a -> UnifyM b -> UnifyM a)
    -> Applicative UnifyM
    forall a. a -> UnifyM a
    forall a b. UnifyM a -> UnifyM b -> UnifyM a
    forall a b. UnifyM a -> UnifyM b -> UnifyM b
    forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
    forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
    forall (f :: * -> *).
    Functor f =>
    (forall a. a -> f a)
    -> (forall a b. f (a -> b) -> f a -> f b)
    -> (forall a b c. (a -> b -> c) -> f a -> f b -> f c)
    -> (forall a b. f a -> f b -> f b)
    -> (forall a b. f a -> f b -> f a)
    -> Applicative f
    $cpure :: forall a. a -> UnifyM a
    pure :: forall a. a -> UnifyM a
    $c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
    <*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
    $cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
    liftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
    $c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
    *> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
    $c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
    <* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
    Applicative,
          MonadState UnifyMState,
          MonadError TypeError
        )

    newVar :: Name -> UnifyM VName
    newVar :: Name -> UnifyM VName
    newVar Name
    name = do
      (Constraints
    x, Int
    i) <- UnifyM (Constraints, Int)
    forall s (m :: * -> *). MonadState s m => m s
    get
      (Constraints, Int) -> UnifyM ()
    forall s (m :: * -> *). MonadState s m => s -> m ()
    put (Constraints
    x, Int
    i Int -> Int -> Int
    forall a. Num a => a -> a -> a
    + Int
    1)
      VName -> UnifyM VName
    forall a. a -> UnifyM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (VName -> UnifyM VName) -> VName -> UnifyM VName
    forall a b. (a -> b) -> a -> b
    $ Name -> Int -> VName
    VName (Name -> Int -> Name
    mkTypeVarName Name
    name Int
    i) Int
    i

    instance MonadUnify UnifyM where
      getConstraints :: UnifyM Constraints
    getConstraints = ((Constraints, Int) -> Constraints) -> UnifyM Constraints
    forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
    gets (Constraints, Int) -> Constraints
    forall a b. (a, b) -> a
    fst
      putConstraints :: Constraints -> UnifyM ()
    putConstraints Constraints
    x = ((Constraints, Int) -> (Constraints, Int)) -> UnifyM ()
    forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
    modify (((Constraints, Int) -> (Constraints, Int)) -> UnifyM ())
    -> ((Constraints, Int) -> (Constraints, Int)) -> UnifyM ()
    forall a b. (a -> b) -> a -> b
    $ \(Constraints
    _, Int
    i) -> (Constraints
    x, Int
    i)

      newTypeVar :: forall als a dim.
    (Monoid als, Located a) =>
    a -> Name -> UnifyM (TypeBase dim als)
    newTypeVar a
    loc Name
    name = do
        VName
    v <- Name -> UnifyM VName
    newVar Name
    name
        (Constraints -> Constraints) -> UnifyM ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
    -> (Constraints -> Constraints) -> UnifyM ()
    forall a b. (a -> b) -> a -> b
    $ VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    v (Int
    0, Liftedness -> Usage -> Constraint
    NoConstraint Liftedness
    Lifted (Usage -> Constraint) -> Usage -> Constraint
    forall a b. (a -> b) -> a -> b
    $ Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing (Loc -> Usage) -> Loc -> Usage
    forall a b. (a -> b) -> a -> b
    $ a -> Loc
    forall a. Located a => a -> Loc
    locOf a
    loc)
        TypeBase dim als -> UnifyM (TypeBase dim als)
    forall a. a -> UnifyM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure (TypeBase dim als -> UnifyM (TypeBase dim als))
    -> TypeBase dim als -> UnifyM (TypeBase dim als)
    forall a b. (a -> b) -> a -> b
    $ ScalarTypeBase dim als -> TypeBase dim als
    forall dim u. ScalarTypeBase dim u -> TypeBase dim u
    Scalar (ScalarTypeBase dim als -> TypeBase dim als)
    -> ScalarTypeBase dim als -> TypeBase dim als
    forall a b. (a -> b) -> a -> b
    $ als -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim als
    forall dim u.
    u -> QualName VName -> [TypeArg dim] -> ScalarTypeBase dim u
    TypeVar als
    forall a. Monoid a => a
    mempty (VName -> QualName VName
    forall v. v -> QualName v
    qualName VName
    v) []

      newDimVar :: Usage -> Rigidity -> Name -> UnifyM VName
    newDimVar Usage
    usage Rigidity
    rigidity Name
    name = do
        VName
    dim <- Name -> UnifyM VName
    newVar Name
    name
        case Rigidity
    rigidity of
          Rigid RigidSource
    src ->
            (Constraints -> Constraints) -> UnifyM ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
    -> (Constraints -> Constraints) -> UnifyM ()
    forall a b. (a -> b) -> a -> b
    $
              VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    dim (Int
    0, Loc -> RigidSource -> Constraint
    UnknownSize (Usage -> Loc
    forall a. Located a => a -> Loc
    locOf Usage
    usage) RigidSource
    src)
          Rigidity
    Nonrigid ->
            (Constraints -> Constraints) -> UnifyM ()
    forall (m :: * -> *).
    MonadUnify m =>
    (Constraints -> Constraints) -> m ()
    modifyConstraints ((Constraints -> Constraints) -> UnifyM ())
    -> (Constraints -> Constraints) -> UnifyM ()
    forall a b. (a -> b) -> a -> b
    $
              VName -> (Int, Constraint) -> Constraints -> Constraints
    forall k a. Ord k => k -> a -> Map k a -> Map k a
    M.insert VName
    dim (Int
    0, Maybe Exp -> Usage -> Constraint
    Size Maybe Exp
    forall a. Maybe a
    Nothing Usage
    usage)
        VName -> UnifyM VName
    forall a. a -> UnifyM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure VName
    dim

      curLevel :: UnifyM Int
    curLevel = Int -> UnifyM Int
    forall a. a -> UnifyM a
    forall (f :: * -> *) a. Applicative f => a -> f a
    pure Int
    1

      unifyError :: forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> Doc () -> UnifyM a
    unifyError loc
    loc Notes
    notes BreadCrumbs
    bcs Doc ()
    doc =
        TypeError -> UnifyM a
    forall a. TypeError -> UnifyM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
    forall a b. (a -> b) -> a -> b
    $ Loc -> Notes -> Doc () -> TypeError
    TypeError (loc -> Loc
    forall a. Located a => a -> Loc
    locOf loc
    loc) Notes
    notes (Doc () -> TypeError) -> Doc () -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Doc ()
    doc Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> BreadCrumbs -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. BreadCrumbs -> Doc ann
    pretty BreadCrumbs
    bcs

      matchError :: forall loc a.
    Located loc =>
    loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
    matchError loc
    loc Notes
    notes BreadCrumbs
    bcs StructType
    t1 StructType
    t2 =
        TypeError -> UnifyM a
    forall a. TypeError -> UnifyM a
    forall e (m :: * -> *) a. MonadError e m => e -> m a
    throwError (TypeError -> UnifyM a) -> TypeError -> UnifyM a
    forall a b. (a -> b) -> a -> b
    $ Loc -> Notes -> Doc () -> TypeError
    TypeError (loc -> Loc
    forall a. Located a => a -> Loc
    locOf loc
    loc) Notes
    notes (Doc () -> TypeError) -> Doc () -> TypeError
    forall a b. (a -> b) -> a -> b
    $ Doc ()
    forall ann. Doc ann
    doc Doc () -> Doc () -> Doc ()
    forall a. Semigroup a => a -> a -> a
    <> BreadCrumbs -> Doc ()
    forall a ann. Pretty a => a -> Doc ann
    forall ann. BreadCrumbs -> Doc ann
    pretty BreadCrumbs
    bcs
        where
          doc :: Doc a
    doc =
            Doc a
    "Types"
              Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc a -> Doc a
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc a
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t1)
              Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    </> Doc a
    "and"
              Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    </> Int -> Doc a -> Doc a
    forall ann. Int -> Doc ann -> Doc ann
    indent Int
    2 (StructType -> Doc a
    forall a ann. Pretty a => a -> Doc ann
    forall ann. StructType -> Doc ann
    pretty StructType
    t2)
              Doc a -> Doc a -> Doc a
    forall a. Doc a -> Doc a -> Doc a
    </> Doc a
    "do not match."

    runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
    runUnifyM :: forall a.
    [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
    runUnifyM [TypeParam]
    rigid_tparams [TypeParam]
    nonrigid_tparams (UnifyM StateT (Constraints, Int) (Except TypeError) a
    m) =
      Except TypeError a -> Either TypeError a
    forall e a. Except e a -> Either e a
    runExcept (Except TypeError a -> Either TypeError a)
    -> Except TypeError a -> Either TypeError a
    forall a b. (a -> b) -> a -> b
    $ StateT (Constraints, Int) (Except TypeError) a
    -> (Constraints, Int) -> Except TypeError a
    forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
    evalStateT StateT (Constraints, Int) (Except TypeError) a
    m (Constraints
    constraints, Int
    0)
      where
        constraints :: Constraints
    constraints =
          [(VName, (Int, Constraint))] -> Constraints
    forall k a. Ord k => [(k, a)] -> Map k a
    M.fromList ([(VName, (Int, Constraint))] -> Constraints)
    -> [(VName, (Int, Constraint))] -> Constraints
    forall a b. (a -> b) -> a -> b
    $
            (TypeParam -> (VName, (Int, Constraint)))
    -> [TypeParam] -> [(VName, (Int, Constraint))]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeParam -> (VName, (Int, Constraint))
    forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
    nonrigid [TypeParam]
    nonrigid_tparams [(VName, (Int, Constraint))]
    -> [(VName, (Int, Constraint))] -> [(VName, (Int, Constraint))]
    forall a. Semigroup a => a -> a -> a
    <> (TypeParam -> (VName, (Int, Constraint)))
    -> [TypeParam] -> [(VName, (Int, Constraint))]
    forall a b. (a -> b) -> [a] -> [b]
    map TypeParam -> (VName, (Int, Constraint))
    forall {a} {a}. Num a => TypeParamBase a -> (a, (a, Constraint))
    rigid [TypeParam]
    rigid_tparams
        nonrigid :: TypeParamBase a -> (a, (a, Constraint))
    nonrigid (TypeParamDim a
    p SrcLoc
    loc) = (a
    p, (a
    1, Maybe Exp -> Usage -> Constraint
    Size Maybe Exp
    forall a. Maybe a
    Nothing (Usage -> Constraint) -> Usage -> Constraint
    forall a b. (a -> b) -> a -> b
    $ Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing (Loc -> Usage) -> Loc -> Usage
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc))
        nonrigid (TypeParamType Liftedness
    l a
    p SrcLoc
    loc) = (a
    p, (a
    1, Liftedness -> Usage -> Constraint
    NoConstraint Liftedness
    l (Usage -> Constraint) -> Usage -> Constraint
    forall a b. (a -> b) -> a -> b
    $ Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing (Loc -> Usage) -> Loc -> Usage
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc))
        rigid :: TypeParamBase a -> (a, (a, Constraint))
    rigid (TypeParamDim a
    p SrcLoc
    loc) = (a
    p, (a
    0, Loc -> Constraint
    ParamSize (Loc -> Constraint) -> Loc -> Constraint
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc))
        rigid (TypeParamType Liftedness
    l a
    p SrcLoc
    loc) = (a
    p, (a
    0, Liftedness -> Loc -> Constraint
    ParamType Liftedness
    l (Loc -> Constraint) -> Loc -> Constraint
    forall a b. (a -> b) -> a -> b
    $ SrcLoc -> Loc
    forall a. Located a => a -> Loc
    locOf SrcLoc
    loc))

    -- | Perform a unification of two types outside a monadic context.
    -- The first list of type parameters are rigid but may have liftedness
    -- constraints; the second list of type parameters are allowed to be
    -- instantiated. All other types are considered rigid with no
    -- constraints.
    doUnification ::
      Loc ->
      [TypeParam] ->
      [TypeParam] ->
      StructType ->
      StructType ->
      Either TypeError StructType
    doUnification :: Loc
    -> [TypeParam]
    -> [TypeParam]
    -> StructType
    -> StructType
    -> Either TypeError StructType
    doUnification Loc
    loc [TypeParam]
    rigid_tparams [TypeParam]
    nonrigid_tparams StructType
    t1 StructType
    t2 =
      [TypeParam]
    -> [TypeParam] -> UnifyM StructType -> Either TypeError StructType
    forall a.
    [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
    runUnifyM [TypeParam]
    rigid_tparams [TypeParam]
    nonrigid_tparams (UnifyM StructType -> Either TypeError StructType)
    -> UnifyM StructType -> Either TypeError StructType
    forall a b. (a -> b) -> a -> b
    $ do
        Usage -> StructType -> StructType -> UnifyM ()
    forall (m :: * -> *).
    MonadUnify m =>
    Usage -> StructType -> StructType -> m ()
    unify (Maybe Text -> Loc -> Usage
    Usage Maybe Text
    forall a. Maybe a
    Nothing (Loc -> Loc
    forall a. Located a => a -> Loc
    locOf Loc
    loc)) StructType
    t1 StructType
    t2
        StructType -> UnifyM StructType
    forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
    normTypeFully StructType
    t2

    -- Note [Linking variables to sum types]
    --
    -- Consider the case when unifying a result type
    --
    --   i32 -> ?[n].(#foo [n]bool)
    --
    -- with
    --
    --   i32 -> ?[k].a
    --
    -- where 'a' has a HasConstrs constraint saying that it must have at
    -- least a constructor of type '#foo [0]bool'.
    --
    -- This unification should succeed, but we must not merely link 'a' to
    -- '#foo [n]bool', as 'n' is not free.  Instead we should instantiate
    -- 'a' to be a concrete sum type (because now we know exactly which
    -- constructor labels it must have), and unify each of its constructor
    -- payloads with the corresponding expected payload.