content: -- | 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 (MatchingTypes t1 t2) =
      "When matching type"
        </> indent 2 (pretty t1)
        </> "with"
        </> indent 2 (pretty t2)
    pretty (MatchingFields fields) =
      "When matching types of record field"
        <+> dquotes (mconcat $ punctuate "." $ map pretty fields)
        <> dot
    pretty (MatchingConstructor c) =
      "When matching types of constructor" <+> dquotes (pretty c) <> dot
    pretty (Matching s) =
      unAnnotate 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 []
  
  -- | Is the path empty?
  hasNoBreadCrumbs :: BreadCrumbs -> Bool
  hasNoBreadCrumbs (BreadCrumbs xs) = null xs
  
  -- | Drop a breadcrumb on the path behind you.
  breadCrumb :: BreadCrumb -> BreadCrumbs -> BreadCrumbs
  breadCrumb (MatchingFields xs) (BreadCrumbs (MatchingFields ys : bcs)) =
    BreadCrumbs $ MatchingFields (ys ++ xs) : bcs
  breadCrumb bc (BreadCrumbs bcs) =
    BreadCrumbs $ bc : bcs
  
  instance Pretty BreadCrumbs where
    pretty (BreadCrumbs []) = mempty
    pretty (BreadCrumbs bcs) = line <> stack (map pretty bcs)
  
  -- | A usage that caused a type constraint.
  data Usage = Usage (Maybe T.Text) Loc
    deriving (Show)
  
  -- | Construct a 'Usage' from a location and a description.
  mkUsage :: (Located a) => a -> T.Text -> Usage
  mkUsage = flip (Usage . Just) . locOf
  
  -- | Construct a 'Usage' that has just a location, but no particular
  -- description.
  mkUsage' :: (Located a) => a -> Usage
  mkUsage' = Usage Nothing . locOf
  
  instance Pretty Usage where
    pretty (Usage Nothing loc) = "use at " <> textwrap (locText loc)
    pretty (Usage (Just s) loc) = textwrap s <+> "at" <+> textwrap (locText loc)
  
  instance Located Usage where
    locOf (Usage _ loc) = locOf 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 (Show)
  
  instance Located Constraint where
    locOf (NoConstraint _ usage) = locOf usage
    locOf (ParamType _ usage) = locOf usage
    locOf (Constraint _ usage) = locOf usage
    locOf (Overloaded _ usage) = locOf usage
    locOf (HasFields _ _ usage) = locOf usage
    locOf (Equality usage) = locOf usage
    locOf (HasConstrs _ _ usage) = locOf usage
    locOf (ParamSize loc) = locOf loc
    locOf (Size _ usage) = locOf usage
    locOf (UnknownSize loc _) = locOf 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 v constraints = case snd <$> M.lookup v constraints of
    Just (Constraint t _) -> Just $ Subst [] $ applySubst (`lookupSubst` constraints) t
    Just (Size (Just d) _) ->
      Just $ ExpSubst $ applySubst (`lookupSubst` constraints) d
    _ -> 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 (Eq, Ord, 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 (Eq, Ord, Show)
  
  prettySource :: Loc -> Loc -> RigidSource -> Doc ()
  prettySource ctx loc (RigidRet Nothing) =
    "is unknown size returned by function at"
      <+> pretty (locStrRel ctx loc)
      <> "."
  prettySource ctx loc (RigidRet (Just fname)) =
    "is unknown size returned by"
      <+> dquotes (pretty fname)
      <+> "at"
      <+> pretty (locStrRel ctx loc)
      <> "."
  prettySource ctx loc (RigidArg fname arg) =
    "is value of argument"
      </> indent 2 (shorten (pretty arg))
      </> "passed to"
      <+> fname'
      <+> "at"
      <+> pretty (locStrRel ctx loc)
      <> "."
    where
      fname' = maybe "function" (dquotes . pretty) fname
  prettySource ctx loc (RigidSlice d slice) =
    "is size produced by slice"
      </> indent 2 (shorten (pretty slice))
      </> d_desc
      <> "at"
        <+> pretty (locStrRel ctx loc)
      <> "."
    where
      d_desc = case d of
        Just d' -> "of dimension of size " <> dquotes (pretty d') <> " "
        Nothing -> mempty
  prettySource ctx loc RigidLoop =
    "is unknown size of value returned at" <+> pretty (locStrRel ctx loc) <> "."
  prettySource ctx loc RigidRange =
    "is unknown length of range at" <+> pretty (locStrRel ctx loc) <> "."
  prettySource ctx loc (RigidOutOfScope boundloc v) =
    "is an unknown size arising from "
      <> dquotes (prettyName v)
      <> " going out of scope at "
      <> pretty (locStrRel ctx loc)
      <> "."
        </> "Originally bound at "
      <> pretty (locStrRel ctx boundloc)
      <> "."
  prettySource _ _ RigidUnify =
    "is an artificial size invented during unification of functions with anonymous sizes."
  prettySource ctx loc (RigidCond t1 t2) =
    "is unknown due to conditional expression at "
      <> pretty (locStrRel ctx loc)
      <> "."
        </> "One branch returns array of type: "
      <> align (pretty t1)
        </> "The other an array of type:       "
      <> align (pretty 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 ctx (Var d _ _) = do
    c <- M.lookup (qualLeaf d) <$> getConstraints
    case c of
      Just (_, UnknownSize loc rsrc) ->
        pure . aNote $
          dquotes (pretty d) <+> prettySource (locOf ctx) loc rsrc
      _ -> pure mempty
  dimNotes _ _ = pure mempty
  
  typeNotes :: (Located a, MonadUnify m) => a -> StructType -> m Notes
  typeNotes ctx =
    fmap mconcat
      . mapM (dimNotes ctx . flip sizeFromName mempty . qualName)
      . S.toList
      . fvVars
      . freeInType
  
  typeVarNotes :: (MonadUnify m) => VName -> m Notes
  typeVarNotes v = maybe mempty (note . snd) . M.lookup v <$> getConstraints
    where
      note (HasConstrs _ cs _) =
        aNote $
          prettyName v
            <+> "="
            <+> hsep (map ppConstr (M.toList cs))
            <+> "..."
      note (Overloaded ts _) =
        aNote $ prettyName v <+> "must be one of" <+> mconcat (punctuate ", " (map pretty ts))
      note (HasFields _ fs _) =
        aNote $
          prettyName v
            <+> "="
            <+> braces (mconcat (punctuate ", " (map ppField (M.toList fs))))
      note _ = mempty
  
      ppConstr (c, _) = "#" <> pretty c <+> "..." <+> "|"
      ppField (f, _) = prettyName f <> ":" <+> "..."
  
  -- | 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 f = do
      x <- getConstraints
      putConstraints $ f 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 loc = newDimVar (mkUsage' loc) . Rigid
    newFlexibleDim :: Usage -> Name -> m VName
    newFlexibleDim usage = newDimVar usage 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 t = do
    constraints <- getConstraints
    pure $ applySubst (`lookupSubst` constraints) t
  
  -- | Replace any top-level type variable with its substitution.
  normType :: (MonadUnify m) => StructType -> m StructType
  normType t@(Scalar (TypeVar _ (QualName [] v) [])) = do
    constraints <- getConstraints
    case snd <$> M.lookup v constraints of
      Just (Constraint (RetType [] t') _) -> normType t'
      _ -> pure t
  normType t = pure t
  
  rigidConstraint :: Constraint -> Bool
  rigidConstraint ParamType {} = True
  rigidConstraint ParamSize {} = True
  rigidConstraint UnknownSize {} = True
  rigidConstraint _ = False
  
  unsharedConstructorsMsg :: M.Map Name t -> M.Map Name t -> Doc a
  unsharedConstructorsMsg cs1 cs2 =
    "Unshared constructors:" <+> commasep (map (("#" <>) . pretty) missing) <> "."
    where
      missing =
        filter (`notElem` M.keys cs1) (M.keys cs2)
          ++ filter (`notElem` M.keys cs2) (M.keys cs1)
  
  -- | Is the given type variable the name of an abstract type or type
  -- parameter, which we cannot substitute?
  isRigid :: VName -> Constraints -> Bool
  isRigid v constraints =
    maybe True (rigidConstraint . snd) $ M.lookup v constraints
  
  -- | If the given type variable is nonrigid, what is its level?
  isNonRigid :: VName -> Constraints -> Maybe Level
  isNonRigid v constraints = do
    (lvl, c) <- M.lookup v constraints
    guard $ not $ rigidConstraint c
    pure lvl
  
  type UnifySizes m =
    BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Exp -> Exp -> m ()
  
  flipUnifySizes :: UnifySizes m -> UnifySizes m
  flipUnifySizes onDims bcs bound nonrigid t1 t2 =
    onDims bcs bound nonrigid t2 t1
  
  unifyWith ::
    (MonadUnify m) =>
    UnifySizes m ->
    Usage ->
    [VName] ->
    BreadCrumbs ->
    StructType ->
    StructType ->
    m ()
  unifyWith onDims usage = subunify False
    where
      swap True x y = (y, x)
      swap False x y = (x, y)
  
      subunify ord bound bcs t1 t2 = do
        constraints <- getConstraints
  
        t1' <- normType t1
        t2' <- normType t2
  
        let nonrigid v = isNonRigid v constraints
  
            failure = matchError (srclocOf usage) mempty bcs t1' t2'
  
            link ord' =
              linkVarToType linkDims usage bound bcs
              where
                -- We may have to flip the order of future calls to
                -- onDims inside linkVarToType.
                linkDims
                  | ord' = flipUnifySizes onDims
                  | otherwise = onDims
  
            unifyTypeArg bcs' (TypeArgDim d1) (TypeArgDim d2) =
              onDims' bcs' (swap ord d1 d2)
            unifyTypeArg bcs' (TypeArgType t) (TypeArgType arg_t) =
              subunify ord bound bcs' t arg_t
            unifyTypeArg bcs' _ _ =
              unifyError
                usage
                mempty
                bcs'
                "Cannot unify a type argument with a dimension argument (or vice versa)."
  
            onDims' bcs' (d1, d2) =
              onDims
                bcs'
                bound
                nonrigid
                (applySubst (`lookupSubst` constraints) d1)
                (applySubst (`lookupSubst` constraints) d2)
  
        case (t1', t2') of
          (Scalar (Prim pt1), Scalar (Prim pt2))
            | pt1 == pt2 -> pure ()
          ( Scalar (Record fs),
            Scalar (Record arg_fs)
            )
              | M.keys fs == M.keys arg_fs ->
                  unifySharedFields onDims usage bound bcs fs arg_fs
              | otherwise -> do
                  let missing =
                        filter (`notElem` M.keys arg_fs) (M.keys fs)
                          ++ filter (`notElem` M.keys fs) (M.keys arg_fs)
                  unifyError usage mempty bcs $
                    "Unshared fields:" <+> commasep (map pretty missing) <> "."
          ( Scalar (TypeVar _ (QualName _ tn) targs),
            Scalar (TypeVar _ (QualName _ arg_tn) arg_targs)
            )
              | tn == arg_tn,
                length targs == length arg_targs -> do
                  let bcs' = breadCrumb (Matching "When matching type arguments.") bcs
                  zipWithM_ (unifyTypeArg bcs') targs arg_targs
          ( Scalar (TypeVar _ (QualName [] v1) []),
            Scalar (TypeVar _ (QualName [] v2) [])
            ) ->
              case (nonrigid v1, nonrigid v2) of
                (Nothing, Nothing) -> failure
                (Just lvl1, Nothing) -> link ord v1 lvl1 t2'
                (Nothing, Just lvl2) -> link (not ord) v2 lvl2 t1'
                (Just lvl1, Just lvl2)
                  | lvl1 <= lvl2 -> link ord v1 lvl1 t2'
                  | otherwise -> link (not ord) v2 lvl2 t1'
          (Scalar (TypeVar _ (QualName [] v1) []), _)
            | Just lvl <- nonrigid v1 ->
                link ord v1 lvl t2'
          (_, Scalar (TypeVar _ (QualName [] v2) []))
            | Just lvl <- nonrigid v2 ->
                link (not ord) v2 lvl t1'
          ( Scalar (Arrow _ p1 d1 a1 (RetType b1_dims b1)),
            Scalar (Arrow _ p2 d2 a2 (RetType b2_dims b2))
            )
              | uncurry (<) $ swap ord d1 d2 -> do
                  unifyError usage mempty bcs . withIndexLink "unify-consuming-param" $
                    "Parameters"
                      </> indent 2 (pretty d1 <> pretty a1)
                      </> "and"
                      </> indent 2 (pretty d2 <> pretty a2)
                      </> "are incompatible regarding consuming their arguments."
              | uncurry (<) $ swap ord (uniqueness b2) (uniqueness b1) -> do
                  unifyError usage mempty bcs . withIndexLink "unify-return-uniqueness" $
                    "Return types"
                      </> indent 2 (pretty b1)
                      </> "and"
                      </> indent 2 (pretty b2)
                      </> "have incompatible uniqueness."
              | otherwise -> do
                  -- Introduce the existentials as size variables so they
                  -- are subject to unification.  We will remove them again
                  -- afterwards.
                  let (r1, r2) =
                        swap
                          ord
                          (Size Nothing $ Usage Nothing mempty)
                          (UnknownSize mempty RigidUnify)
                  lvl <- curLevel
                  modifyConstraints (M.fromList (map (,(lvl, r1)) b1_dims) <>)
                  modifyConstraints (M.fromList (map (,(lvl, r2)) b2_dims) <>)
  
                  let bound' = bound <> mapMaybe pname [p1, p2] <> b1_dims <> b2_dims
                  subunify
                    (not ord)
                    bound
                    (breadCrumb (Matching "When matching parameter types.") bcs)
                    a1
                    a2
                  subunify
                    ord
                    bound'
                    (breadCrumb (Matching "When matching return types.") bcs)
                    (toStruct b1')
                    (toStruct b2')
  
                  -- Delete the size variables we introduced to represent
                  -- the existential sizes.
                  modifyConstraints $ \m -> L.foldl' (flip M.delete) m (b1_dims <> b2_dims)
              where
                (b1', 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 (p1, p2) of
                    (Named p1', Named p2') ->
                      let f v
                            | v == p2' = Just $ ExpSubst $ sizeFromName (qualName p1') mempty
                            | otherwise = Nothing
                       in (b1, applySubst f b2)
                    (_, _) ->
                      (b1, b2)
  
                pname (Named x) = Just x
                pname Unnamed = Nothing
          (Array {}, Array {})
            | Shape (t1_d : _) <- arrayShape t1',
              Shape (t2_d : _) <- arrayShape t2',
              Just t1'' <- peelArray 1 t1',
              Just t2'' <- peelArray 1 t2' -> do
                onDims' bcs (swap ord t1_d t2_d)
                subunify ord bound bcs t1'' t2''
          ( Scalar (Sum cs),
            Scalar (Sum arg_cs)
            )
              | M.keys cs == M.keys arg_cs ->
                  unifySharedConstructors onDims usage bound bcs cs arg_cs
              | otherwise ->
                  unifyError usage mempty bcs $ unsharedConstructorsMsg arg_cs cs
          _ -> failure
  
  anyBound :: [VName] -> ExpBase Info VName -> Bool
  anyBound bound e = any (`S.member` fvVars (freeInExp e)) bound
  
  unifySizes :: (MonadUnify m) => Usage -> UnifySizes m
  unifySizes usage bcs bound nonrigid e1 e2
    | Just es <- similarExps e1 e2 =
        mapM_ (uncurry $ unifySizes usage bcs bound nonrigid) es
  unifySizes usage bcs bound nonrigid (Var v1 _ _) e2
    | Just lvl1 <- nonrigid (qualLeaf v1),
      not (anyBound bound e2) || (qualLeaf v1 `elem` bound) =
        linkVarToDim usage bcs (qualLeaf v1) lvl1 e2
  unifySizes usage bcs bound nonrigid e1 (Var v2 _ _)
    | Just lvl2 <- nonrigid (qualLeaf v2),
      not (anyBound bound e1) || (qualLeaf v2 `elem` bound) =
        linkVarToDim usage bcs (qualLeaf v2) lvl2 e1
  unifySizes usage bcs _ _ e1 e2 = do
    notes <- (<>) <$> dimNotes usage e1 <*> dimNotes usage e2
    unifyError usage notes bcs $
      "Sizes"
        <+> dquotes (pretty e1)
        <+> "and"
        <+> dquotes (pretty e2)
        <+> "do not match."
  
  -- | Unifies two types.
  unify :: (MonadUnify m) => Usage -> StructType -> StructType -> m ()
  unify usage = unifyWith (unifySizes usage) usage mempty noBreadCrumbs
  
  occursCheck ::
    (MonadUnify m) =>
    Usage ->
    BreadCrumbs ->
    VName ->
    StructType ->
    m ()
  occursCheck usage bcs vn tp =
    when (vn `S.member` typeVars tp) $
      unifyError usage mempty bcs $
        "Occurs check: cannot instantiate"
          <+> prettyName vn
          <+> "with"
          <+> pretty tp
          <> "."
  
  scopeCheck ::
    (MonadUnify m) =>
    Usage ->
    BreadCrumbs ->
    VName ->
    Level ->
    StructType ->
    m ()
  scopeCheck usage bcs vn max_lvl tp = do
    constraints <- getConstraints
    checkType constraints tp
    where
      checkType constraints t =
        mapM_ (check constraints) $ typeVars t <> fvVars (freeInType t)
  
      check constraints v
        | Just (lvl, c) <- M.lookup v constraints,
          lvl > max_lvl =
            if rigidConstraint c
              then scopeViolation v
              else modifyConstraints $ M.insert v (max_lvl, c)
        | otherwise =
            pure ()
  
      scopeViolation v = do
        notes <- typeNotes usage tp
        unifyError usage notes bcs $
          "Cannot unify type"
            </> indent 2 (pretty tp)
            </> "with"
            <+> dquotes (prettyName vn)
            <+> "(scope violation)."
            </> "This is because"
            <+> dquotes (prettyName v)
            <+> "is rigidly bound in a deeper scope."
  
  -- Expressions witnessed by type, topologically sorted.
  topWit :: TypeBase Exp u -> [Exp]
  topWit = topologicalSort depends . witnessedExps
    where
      witnessedExps t = execState (traverseDims onDim t) mempty
        where
          onDim _ PosImmediate e = modify (e :)
          onDim _ _ _ = pure ()
      depends a b = any (sameExp b) $ subExps a
  
  sizeFree ::
    (MonadUnify m) =>
    SrcLoc ->
    (Exp -> Maybe VName) ->
    TypeBase Size u ->
    m (TypeBase Size u, [VName])
  sizeFree tloc expKiller orig_t = do
    runReaderT (toBeReplaced orig_t $ onType orig_t) mempty `runStateT` mempty
    where
      lookReplacement e repl = snd <$> L.find (sameExp e . fst) repl
      expReplace mapping e
        | Just e' <- lookReplacement e mapping = e'
        | otherwise = runIdentity $ astMap mapper e
        where
          mapper = identityMapper {mapOnExp = pure . expReplace mapping}
  
      replacing e = do
        e' <- asks (`expReplace` e)
        case expKiller e' of
          Nothing -> pure e'
          Just cause -> do
            vn <- lift $ lift $ newRigidDim tloc (RigidOutOfScope (locOf e) cause) "d"
            modify (vn :)
            pure $ sizeFromName (qualName vn) (srclocOf e)
  
      toBeReplaced t m' = foldl f m' $ topWit t
        where
          f m e = do
            e' <- replacing e
            local ((e, e') :) m
  
      onScalar (Record fs) =
        Record <$> traverse onType fs
      onScalar (Sum cs) =
        Sum <$> (traverse . traverse) onType cs
      onScalar (Arrow as pn d argT (RetType dims retT)) = do
        argT' <- onType argT
        old_bound <- get
        retT' <- toBeReplaced retT $ onType retT
        rl <- state $ L.partition (`notElem` old_bound)
        let dims' = dims <> rl
        pure $ Arrow as pn d argT' (RetType dims' retT')
      onScalar (TypeVar u v args) =
        TypeVar u v <$> mapM onTypeArg args
        where
          onTypeArg (TypeArgDim d) = TypeArgDim <$> replacing d
          onTypeArg (TypeArgType ty) = TypeArgType <$> onType ty
      onScalar (Prim pt) = pure $ Prim pt
  
      onType ::
        (MonadUnify m) =>
        TypeBase Size u ->
        ReaderT [(Exp, Exp)] (StateT [VName] m) (TypeBase Size u)
      onType (Array u shape scalar) =
        Array u <$> traverse replacing shape <*> onScalar scalar
      onType (Scalar ty) =
        Scalar <$> onScalar ty
  
  linkVarToType ::
    (MonadUnify m) =>
    UnifySizes m ->
    Usage ->
    [VName] ->
    BreadCrumbs ->
    VName ->
    Level ->
    StructType ->
    m ()
  linkVarToType onDims usage bound bcs vn lvl tp_unnorm = do
    -- We have to expand anyway for the occurs check, so we might as
    -- well link the fully expanded type.
    tp <- normTypeFully tp_unnorm
    occursCheck usage bcs vn tp
    scopeCheck usage bcs vn lvl tp
  
    let link = do
          let (witnessed, not_witnessed) = determineSizeWitnesses tp
              used v = v `S.member` witnessed || v `S.member` not_witnessed
              (ext_witnessed, ext_not_witnessed) =
                L.partition (`elem` witnessed) $ filter used bound
  
              -- Any size that uses an ext_not_witnessed variable must
              -- be replaced with a fresh existential.
              problematic e =
                L.find (`elem` ext_not_witnessed) $
                  S.toList $
                    fvVars $
                      freeInExp e
  
          (tp', ext_new) <- sizeFree (srclocOf usage) problematic tp
  
          modifyConstraints $
            M.insert vn (lvl, Constraint (RetType (ext_new <> ext_witnessed) tp') usage)
  
    let unliftedBcs unlifted_usage =
          breadCrumb
            ( Matching $
                "When verifying that"
                  <+> dquotes (prettyName vn)
                  <+> textwrap "is not instantiated with a function type, due to"
                  <+> pretty unlifted_usage
            )
            bcs
  
    constraints <- getConstraints
    case snd <$> M.lookup vn constraints of
      Just (NoConstraint Unlifted unlift_usage) -> do
        link
  
        arrayElemTypeWith usage (unliftedBcs unlift_usage) tp
        when (any (`elem` bound) (fvVars (freeInType tp))) $
          unifyError usage mempty bcs $
            "Type variable"
              <+> prettyName vn
              <+> "cannot be instantiated with type containing anonymous sizes:"
              </> indent 2 (pretty tp)
              </> textwrap "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 _) -> do
        link
        equalityType usage tp
      Just (Overloaded ts old_usage)
        | tp `notElem` map (Scalar . Prim) ts -> do
            link
            case tp of
              Scalar (TypeVar _ (QualName [] v) [])
                | not $ isRigid v constraints ->
                    linkVarToTypes usage v ts
              _ ->
                unifyError usage mempty bcs $
                  "Cannot instantiate"
                    <+> dquotes (prettyName vn)
                    <+> "with type"
                    </> indent 2 (pretty tp)
                    </> "as"
                    <+> dquotes (prettyName vn)
                    <+> "must be one of"
                    <+> commasep (map pretty ts)
                    </> "due to"
                    <+> pretty old_usage
                    <> "."
      Just (HasFields l required_fields old_usage) -> do
        when (l == Unlifted) $ arrayElemTypeWith usage (unliftedBcs old_usage) tp
        case tp of
          Scalar (Record tp_fields)
            | all (`M.member` tp_fields) $ M.keys required_fields -> do
                required_fields' <- mapM normTypeFully required_fields
                let tp' = Scalar $ Record $ required_fields <> tp_fields -- Crucially left-biased.
                    ext = filter (`S.member` fvVars (freeInType tp')) bound
                modifyConstraints $
                  M.insert vn (lvl, Constraint (RetType ext tp') usage)
                unifySharedFields onDims usage bound bcs required_fields' tp_fields
          Scalar (TypeVar _ (QualName [] v) []) -> do
            case M.lookup v constraints of
              Just (_, HasFields _ tp_fields _) ->
                unifySharedFields onDims usage bound bcs required_fields tp_fields
              Just (_, NoConstraint {}) -> pure ()
              Just (_, Equality {}) -> pure ()
              _ -> do
                notes <- (<>) <$> typeVarNotes vn <*> typeVarNotes v
                noRecordType notes
            link
            modifyConstraints $
              M.insertWith
                combineFields
                v
                (lvl, HasFields l required_fields old_usage)
            where
              combineFields (_, HasFields l1 fs1 usage1) (_, HasFields l2 fs2 _) =
                (lvl, HasFields (l1 `min` l2) (M.union fs1 fs2) usage1)
              combineFields hasfs _ = hasfs
          _ ->
            unifyError usage mempty bcs $
              "Cannot instantiate"
                <+> dquotes (prettyName vn)
                <+> "with type"
                </> indent 2 (pretty tp)
                </> "as"
                <+> dquotes (prettyName vn)
                <+> "must be a record with fields"
                </> indent 2 (pretty (Record required_fields))
                </> "due to"
                <+> pretty old_usage
                <> "."
      -- See Note [Linking variables to sum types]
      Just (HasConstrs l required_cs old_usage) -> do
        when (l == Unlifted) $ arrayElemTypeWith usage (unliftedBcs old_usage) tp
        case tp of
          Scalar (Sum ts)
            | all (`M.member` ts) $ M.keys required_cs -> do
                let tp' = Scalar $ Sum $ required_cs <> ts -- Crucially left-biased.
                    ext = filter (`S.member` fvVars (freeInType tp')) bound
                modifyConstraints $
                  M.insert vn (lvl, Constraint (RetType ext tp') usage)
                unifySharedConstructors onDims usage bound bcs required_cs ts
            | otherwise ->
                unsharedConstructors required_cs ts =<< typeVarNotes vn
          Scalar (TypeVar _ (QualName [] v) []) -> do
            case M.lookup v constraints of
              Just (_, HasConstrs _ v_cs _) ->
                unifySharedConstructors onDims usage bound bcs required_cs v_cs
              Just (_, NoConstraint {}) -> pure ()
              Just (_, Equality {}) -> pure ()
              _ -> do
                notes <- (<>) <$> typeVarNotes vn <*> typeVarNotes v
                noSumType notes
            link
            modifyConstraints $
              M.insertWith
                combineConstrs
                v
                (lvl, HasConstrs l required_cs old_usage)
            where
              combineConstrs (_, HasConstrs l1 cs1 usage1) (_, HasConstrs l2 cs2 _) =
                (lvl, HasConstrs (l1 `min` l2) (M.union cs1 cs2) usage1)
              combineConstrs hasCs _ = hasCs
          _ -> noSumType =<< typeVarNotes vn
      _ -> link
    where
      unsharedConstructors cs1 cs2 notes =
        unifyError
          usage
          notes
          bcs
          (unsharedConstructorsMsg cs1 cs2)
      noSumType notes =
        unifyError
          usage
          notes
          bcs
          "Cannot unify a sum type with a non-sum type."
      noRecordType notes =
        unifyError
          usage
          notes
          bcs
          "Cannot unify a record type with a non-record type."
  
  linkVarToDim ::
    (MonadUnify m) =>
    Usage ->
    BreadCrumbs ->
    VName ->
    Level ->
    Exp ->
    m ()
  linkVarToDim usage bcs vn lvl e = do
    constraints <- getConstraints
  
    mapM_ (checkVar constraints) $ fvVars $ freeInExp e
  
    modifyConstraints $ M.insert vn (lvl, Size (Just e) usage)
    where
      checkVar _ dim'
        | vn == dim' = do
            notes <- dimNotes usage e
            unifyError usage notes bcs $
              "Occurs check: cannot instantiate"
                <+> dquotes (prettyName vn)
                <+> "with"
                <+> dquotes (pretty e)
                <+> "."
      checkVar constraints dim'
        | Just (dim_lvl, c) <- dim' `M.lookup` constraints,
          dim_lvl >= lvl =
            case c of
              ParamSize {} -> do
                notes <- dimNotes usage e
                unifyError usage notes bcs $
                  "Cannot link size"
                    <+> dquotes (prettyName vn)
                    <+> "to"
                    <+> dquotes (pretty e)
                    <+> "(scope violation)."
                    </> "This is because"
                    <+> dquotes (pretty $ qualName dim')
                    <+> "is not in scope when"
                    <+> dquotes (prettyName vn)
                    <+> "is introduced."
              _ -> modifyConstraints $ M.insert dim' (lvl, c)
      checkVar _ _ = pure ()
  
  -- | Assert that this type must be one of the given primitive types.
  mustBeOneOf :: (MonadUnify m) => [PrimType] -> Usage -> StructType -> m ()
  mustBeOneOf [req_t] usage t = unify usage (Scalar (Prim req_t)) t
  mustBeOneOf ts usage t = do
    t' <- normType t
    constraints <- getConstraints
    let isRigid' v = isRigid v constraints
  
    case t' of
      Scalar (TypeVar _ (QualName [] v) [])
        | not $ isRigid' v -> linkVarToTypes usage v ts
      Scalar (Prim pt) | pt `elem` ts -> pure ()
      _ -> failure
    where
      failure =
        unifyError usage mempty noBreadCrumbs $
          "Cannot unify type"
            <+> dquotes (pretty t)
            <+> "with any of "
            <> commasep (map pretty ts)
            <> "."
  
  linkVarToTypes :: (MonadUnify m) => Usage -> VName -> [PrimType] -> m ()
  linkVarToTypes usage vn ts = do
    vn_constraint <- M.lookup vn <$> getConstraints
    case vn_constraint of
      Just (lvl, Overloaded vn_ts vn_usage) ->
        case ts `L.intersect` vn_ts of
          [] ->
            unifyError usage mempty noBreadCrumbs $
              "Type constrained to one of"
                <+> commasep (map pretty ts)
                <+> "but also one of"
                <+> commasep (map pretty vn_ts)
                <+> "due to"
                <+> pretty vn_usage
                <> "."
          ts' -> modifyConstraints $ M.insert vn (lvl, Overloaded ts' usage)
      Just (_, HasConstrs _ _ vn_usage) ->
        unifyError usage mempty noBreadCrumbs $
          "Type constrained to one of"
            <+> commasep (map pretty ts)
            <> ", but also inferred to be sum type due to"
              <+> pretty vn_usage
            <> "."
      Just (_, HasFields _ _ vn_usage) ->
        unifyError usage mempty noBreadCrumbs $
          "Type constrained to one of"
            <+> commasep (map pretty ts)
            <> ", but also inferred to be record due to"
              <+> pretty vn_usage
            <> "."
      Just (lvl, _) -> modifyConstraints $ M.insert vn (lvl, Overloaded ts usage)
      Nothing ->
        unifyError usage mempty noBreadCrumbs $
          "Cannot constrain type to one of" <+> commasep (map pretty ts)
  
  -- | Assert that this type must support equality.
  equalityType ::
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage ->
    TypeBase dim u ->
    m ()
  equalityType usage t = do
    unless (orderZero t) $
      unifyError usage mempty noBreadCrumbs $
        "Type " <+> dquotes (pretty t) <+> "does not support equality (may contain function)."
    mapM_ mustBeEquality $ typeVars t
    where
      mustBeEquality vn = do
        constraints <- getConstraints
        case M.lookup vn constraints of
          Just (_, Constraint (RetType [] (Scalar (TypeVar _ (QualName [] vn') []))) _) ->
            mustBeEquality vn'
          Just (_, Constraint (RetType _ vn_t) cusage)
            | not $ orderZero vn_t ->
                unifyError usage mempty noBreadCrumbs $
                  "Type"
                    <+> dquotes (pretty t)
                    <+> "does not support equality."
                    </> "Constrained to be higher-order due to"
                    <+> pretty cusage
                    <+> "."
            | otherwise -> pure ()
          Just (lvl, NoConstraint _ _) ->
            modifyConstraints $ M.insert vn (lvl, Equality usage)
          Just (_, Overloaded _ _) ->
            pure () -- All primtypes support equality.
          Just (_, Equality {}) ->
            pure ()
          _ ->
            unifyError usage mempty noBreadCrumbs $
              "Type" <+> prettyName vn <+> "does not support equality."
  
  zeroOrderTypeWith ::
    (MonadUnify m) =>
    Usage ->
    BreadCrumbs ->
    StructType ->
    m ()
  zeroOrderTypeWith usage bcs t = do
    unless (orderZero t) $
      unifyError usage mempty bcs $
        "Type" </> indent 2 (pretty t) </> "found to be functional."
    mapM_ mustBeZeroOrder . S.toList . typeVars =<< normType t
    where
      mustBeZeroOrder vn = do
        constraints <- getConstraints
        case M.lookup vn constraints of
          Just (lvl, NoConstraint _ _) ->
            modifyConstraints $ M.insert vn (lvl, NoConstraint Unlifted usage)
          Just (lvl, HasFields _ fs _) ->
            modifyConstraints $ M.insert vn (lvl, HasFields Unlifted fs usage)
          Just (lvl, HasConstrs _ cs _) ->
            modifyConstraints $ M.insert vn (lvl, HasConstrs Unlifted cs usage)
          Just (_, ParamType Lifted ploc) ->
            unifyError usage mempty bcs $
              "Type parameter"
                <+> dquotes (prettyName vn)
                <+> "at"
                <+> pretty (locStr ploc)
                <+> "may be a function."
          _ -> pure ()
  
  -- | Assert that this type must be zero-order.
  zeroOrderType ::
    (MonadUnify m) => Usage -> T.Text -> StructType -> m ()
  zeroOrderType usage desc =
    zeroOrderTypeWith usage $ breadCrumb bc noBreadCrumbs
    where
      bc = Matching $ "When checking" <+> textwrap desc
  
  arrayElemTypeWith ::
    (MonadUnify m, Pretty (Shape dim), Pretty u) =>
    Usage ->
    BreadCrumbs ->
    TypeBase dim u ->
    m ()
  arrayElemTypeWith usage bcs t = do
    unless (orderZero t) $
      unifyError usage mempty bcs $
        "Type" </> indent 2 (pretty t) </> "found to be functional."
    mapM_ mustBeZeroOrder . S.toList . typeVars $ t
    where
      mustBeZeroOrder vn = do
        constraints <- getConstraints
        case M.lookup vn constraints of
          Just (lvl, NoConstraint _ _) ->
            modifyConstraints $ M.insert vn (lvl, NoConstraint Unlifted usage)
          Just (_, ParamType l ploc)
            | l `elem` [Lifted, SizeLifted] ->
                unifyError usage mempty bcs $
                  "Type parameter"
                    <+> dquotes (prettyName vn)
                    <+> "bound at"
                    <+> pretty (locStr ploc)
                    <+> "is lifted and cannot be an array element."
          _ -> 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 usage desc =
    arrayElemTypeWith usage $ breadCrumb bc noBreadCrumbs
    where
      bc = Matching $ "When checking" <+> textwrap desc
  
  unifySharedFields ::
    (MonadUnify m) =>
    UnifySizes m ->
    Usage ->
    [VName] ->
    BreadCrumbs ->
    M.Map Name StructType ->
    M.Map Name StructType ->
    m ()
  unifySharedFields onDims usage bound bcs fs1 fs2 =
    forM_ (M.toList $ M.intersectionWith (,) fs1 fs2) $ \(f, (t1, t2)) ->
      unifyWith onDims usage bound (breadCrumb (MatchingFields [f]) bcs) t1 t2
  
  unifySharedConstructors ::
    (MonadUnify m) =>
    UnifySizes m ->
    Usage ->
    [VName] ->
    BreadCrumbs ->
    M.Map Name [StructType] ->
    M.Map Name [StructType] ->
    m ()
  unifySharedConstructors onDims usage bound bcs cs1 cs2 =
    forM_ (M.toList $ M.intersectionWith (,) cs1 cs2) $ \(c, (f1, f2)) ->
      unifyConstructor c f1 f2
    where
      unifyConstructor c f1 f2
        | length f1 == length f2 = do
            let bcs' = breadCrumb (MatchingConstructor c) bcs
            zipWithM_ (unifyWith onDims usage bound bcs') f1 f2
        | otherwise =
            unifyError usage mempty bcs $
              "Cannot unify constructor" <+> dquotes (prettyName c) <> "."
  
  -- | 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 usage c t fs = do
    constraints <- getConstraints
    case t of
      Scalar (TypeVar _ (QualName _ tn) [])
        | Just (lvl, NoConstraint l _) <- M.lookup tn constraints -> do
            mapM_ (scopeCheck usage noBreadCrumbs tn lvl) fs
            modifyConstraints $ M.insert tn (lvl, HasConstrs l (M.singleton c fs) usage)
        | Just (lvl, HasConstrs l cs _) <- M.lookup tn constraints ->
            case M.lookup c cs of
              Nothing ->
                modifyConstraints $
                  M.insert tn (lvl, HasConstrs l (M.insert c fs cs) usage)
              Just fs'
                | length fs == length fs' -> zipWithM_ (unify usage) fs fs'
                | otherwise ->
                    unifyError usage mempty noBreadCrumbs $
                      "Different arity for constructor" <+> dquotes (pretty c) <> "."
      Scalar (Sum cs) ->
        case M.lookup c cs of
          Nothing ->
            unifyError usage mempty noBreadCrumbs $
              "Constuctor" <+> dquotes (pretty c) <+> "not present in type."
          Just fs'
            | length fs == length fs' -> zipWithM_ (unify usage) fs fs'
            | otherwise ->
                unifyError usage mempty noBreadCrumbs $
                  "Different arity for constructor" <+> dquotes (pretty c) <+> "."
      _ ->
        unify usage t $ Scalar $ Sum $ M.singleton c fs
  
  mustHaveFieldWith ::
    (MonadUnify m) =>
    UnifySizes m ->
    Usage ->
    [VName] ->
    BreadCrumbs ->
    Name ->
    StructType ->
    m StructType
  mustHaveFieldWith onDims usage bound bcs l t = do
    constraints <- getConstraints
    l_type <- newTypeVar (locOf usage) "t"
    case t of
      Scalar (TypeVar _ (QualName _ tn) [])
        | Just (lvl, NoConstraint {}) <- M.lookup tn constraints -> do
            scopeCheck usage bcs tn lvl l_type
            modifyConstraints $ M.insert tn (lvl, HasFields Lifted (M.singleton l l_type) usage)
            pure l_type
        | Just (lvl, HasFields lifted fields _) <- M.lookup tn constraints -> do
            case M.lookup l fields of
              Just t' -> unifyWith onDims usage bound bcs l_type t'
              Nothing ->
                modifyConstraints $
                  M.insert
                    tn
                    (lvl, HasFields lifted (M.insert l l_type fields) usage)
            pure l_type
      Scalar (Record fields)
        | Just t' <- M.lookup l fields -> do
            unify usage l_type t'
            pure t'
        | otherwise ->
            unifyError usage mempty bcs $
              "Attempt to access field"
                <+> dquotes (pretty l)
                <+> " of value of type"
                <+> pretty (toStructural t)
                <> "."
      _ -> do
        unify usage t $ Scalar $ Record $ M.singleton l l_type
        pure l_type
  
  -- | Assert that some type must have a field with this name and type.
  mustHaveField ::
    (MonadUnify m) =>
    Usage ->
    Name ->
    StructType ->
    m StructType
  mustHaveField usage = mustHaveFieldWith (unifySizes usage) usage mempty noBreadCrumbs
  
  newDimOnMismatch ::
    (MonadUnify m) =>
    Loc ->
    StructType ->
    StructType ->
    m (StructType, [VName])
  newDimOnMismatch loc t1 t2 = do
    (t, seen) <- runStateT (matchDims onDims t1 t2) mempty
    pure (t, M.elems seen)
    where
      r = RigidCond t1 t2
      same (e1, e2) =
        maybe False (all same) $ similarExps e1 e2
      onDims _ d1 d2
        | same (d1, d2) = pure d1
        | otherwise = do
            -- Remember mismatches we have seen before and reuse the
            -- same new size.
            maybe_d <- gets $ M.lookup (d1, d2)
            case maybe_d of
              Just d -> pure $ sizeFromName (qualName d) $ srclocOf loc
              Nothing -> do
                d <- lift $ newRigidDim loc r "differ"
                modify $ M.insert (d1, d2) d
                pure $ sizeFromName (qualName d) $ srclocOf 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 usage t1 t2 = do
    -- We are ignoring the dimensions here, because any mismatches
    -- should be turned into fresh size variables.
    let allOK _ _ _ _ _ = pure ()
    unifyWith allOK usage mempty noBreadCrumbs t1 t2
    t1' <- normTypeFully t1
    t2' <- normTypeFully t2
    newDimOnMismatch (locOf usage) t1' t2'
  
  -- Simple MonadUnify implementation.
  
  type UnifyMState = (Constraints, Int)
  
  newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
    deriving
      ( Monad,
        Functor,
        Applicative,
        MonadState UnifyMState,
        MonadError TypeError
      )
  
  newVar :: Name -> UnifyM VName
  newVar name = do
    (x, i) <- get
    put (x, i + 1)
    pure $ VName (mkTypeVarName name i) i
  
  instance MonadUnify UnifyM where
    getConstraints = gets fst
    putConstraints x = modify $ \(_, i) -> (x, i)
  
    newTypeVar loc name = do
      v <- newVar name
      modifyConstraints $ M.insert v (0, NoConstraint Lifted $ Usage Nothing $ locOf loc)
      pure $ Scalar $ TypeVar mempty (qualName v) []
  
    newDimVar usage rigidity name = do
      dim <- newVar name
      case rigidity of
        Rigid src ->
          modifyConstraints $
            M.insert dim (0, UnknownSize (locOf usage) src)
        Nonrigid ->
          modifyConstraints $
            M.insert dim (0, Size Nothing usage)
      pure dim
  
    curLevel = pure 1
  
    unifyError loc notes bcs doc =
      throwError $ TypeError (locOf loc) notes $ doc <> pretty bcs
  
    matchError loc notes bcs t1 t2 =
      throwError $ TypeError (locOf loc) notes $ doc <> pretty bcs
      where
        doc =
          "Types"
            </> indent 2 (pretty t1)
            </> "and"
            </> indent 2 (pretty t2)
            </> "do not match."
  
  runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
  runUnifyM rigid_tparams nonrigid_tparams (UnifyM m) =
    runExcept $ evalStateT m (constraints, 0)
    where
      constraints =
        M.fromList $
          map nonrigid nonrigid_tparams <> map rigid rigid_tparams
      nonrigid (TypeParamDim p loc) = (p, (1, Size Nothing $ Usage Nothing $ locOf loc))
      nonrigid (TypeParamType l p loc) = (p, (1, NoConstraint l $ Usage Nothing $ locOf loc))
      rigid (TypeParamDim p loc) = (p, (0, ParamSize $ locOf loc))
      rigid (TypeParamType l p loc) = (p, (0, ParamType l $ locOf 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 rigid_tparams nonrigid_tparams t1 t2 =
    runUnifyM rigid_tparams nonrigid_tparams $ do
      unify (Usage Nothing (locOf loc)) t1 t2
      normTypeFully 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.
  