{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE Trustworthy #-}

-- | 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,
    noBreadCrumbs,
    hasNoBreadCrumbs,
    dimNotes,
    zeroOrderType,
    arrayElemType,
    mustHaveConstr,
    mustHaveField,
    mustBeOneOf,
    equalityType,
    normPatType,
    normTypeFully,
    instantiateEmptyArrayDims,
    unify,
    expect,
    unifyMostCommon,
    doUnification,
  )
where

import Control.Monad.Except
import Control.Monad.State
import Data.Bifunctor
import Data.Char (isAscii)
import Data.List (foldl', intersect)
import qualified Data.Map.Strict as M
import Data.Maybe
import qualified Data.Set as S
import Futhark.Util.Pretty hiding (empty)
import Language.Futhark
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
  ppr :: BreadCrumb -> Doc
ppr (MatchingTypes StructType
t1 StructType
t2) =
    Doc
"When matching type"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
      Doc -> Doc -> Doc
</> Doc
"with"
      Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t2)
  ppr (MatchingFields [Name]
fields) =
    Doc
"When matching types of record field"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote ([Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ Doc -> [Doc] -> [Doc]
punctuate Doc
"." ([Doc] -> [Doc]) -> [Doc] -> [Doc]
forall a b. (a -> b) -> a -> b
$ (Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
ppr [Name]
fields) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
  ppr (MatchingConstructor Name
c) =
    Doc
"When matching types of constructor" Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
dot
  ppr (Matching Doc
s) =
    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 (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
  ppr :: BreadCrumbs -> Doc
ppr (BreadCrumbs []) = Doc
forall a. Monoid a => a
mempty
  ppr (BreadCrumbs [BreadCrumb]
bcs) = Doc
line Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
stack ((BreadCrumb -> Doc) -> [BreadCrumb] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map BreadCrumb -> Doc
forall a. Pretty a => a -> Doc
ppr [BreadCrumb]
bcs)

-- | A usage that caused a type constraint.
data Usage = Usage (Maybe String) SrcLoc
  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
showList :: [Usage] -> ShowS
$cshowList :: [Usage] -> ShowS
show :: Usage -> String
$cshow :: Usage -> String
showsPrec :: Int -> Usage -> ShowS
$cshowsPrec :: Int -> Usage -> ShowS
Show)

-- | Construct a 'Usage' from a location and a description.
mkUsage :: SrcLoc -> String -> Usage
mkUsage :: SrcLoc -> String -> Usage
mkUsage = (String -> SrcLoc -> Usage) -> SrcLoc -> String -> Usage
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Maybe String -> SrcLoc -> Usage
Usage (Maybe String -> SrcLoc -> Usage)
-> (String -> Maybe String) -> String -> SrcLoc -> Usage
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Maybe String
forall a. a -> Maybe a
Just)

-- | Construct a 'Usage' that has just a location, but no particular
-- description.
mkUsage' :: SrcLoc -> Usage
mkUsage' :: SrcLoc -> Usage
mkUsage' = Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing

instance Pretty Usage where
  ppr :: Usage -> Doc
ppr (Usage Maybe String
Nothing SrcLoc
loc) = Doc
"use at " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
textwrap (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
loc)
  ppr (Usage (Just String
s) SrcLoc
loc) = String -> Doc
textwrap String
s Doc -> Doc -> Doc
<+/> Doc
"at" Doc -> Doc -> Doc
<+> String -> Doc
textwrap (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
loc)

instance Located Usage where
  locOf :: Usage -> Loc
locOf (Usage Maybe String
_ SrcLoc
loc) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
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 SrcLoc
  | Constraint StructRetType Usage
  | Overloaded [PrimType] Usage
  | HasFields (M.Map Name StructType) Usage
  | Equality Usage
  | HasConstrs (M.Map Name [StructType]) Usage
  | ParamSize SrcLoc
  | -- | Is not actually a type, but a term-level size,
    -- possibly already set to something specific.
    Size (Maybe Size) 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.
    UnknowableSize SrcLoc 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
showList :: [Constraint] -> ShowS
$cshowList :: [Constraint] -> ShowS
show :: Constraint -> String
$cshow :: Constraint -> String
showsPrec :: Int -> Constraint -> ShowS
$cshowsPrec :: Int -> 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
_ SrcLoc
usage) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
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 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 Map Name [StructType]
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (ParamSize SrcLoc
loc) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
loc
  locOf (Size Maybe Size
_ Usage
usage) = Usage -> Loc
forall a. Located a => a -> Loc
locOf Usage
usage
  locOf (UnknowableSize SrcLoc
loc RigidSource
_) = SrcLoc -> Loc
forall a. Located a => a -> Loc
locOf SrcLoc
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 Overloaded {} -> Subst StructRetType -> Maybe (Subst StructRetType)
forall a. a -> Maybe a
Just Subst StructRetType
forall t. Subst t
PrimSubst
  Just (Size (Just Size
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
$ Size -> Subst StructRetType
forall t. Size -> Subst t
SizeSubst (Size -> Subst StructRetType) -> Size -> Subst StructRetType
forall a b. (a -> b) -> a -> b
$ TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
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)) String
  | -- | An existential return size.
    RigidRet (Maybe (QualName VName))
  | RigidLoop
  | -- | Produced by a complicated slice expression.
    RigidSlice (Maybe Size) String
  | -- | Produced by a complicated range expression.
    RigidRange
  | -- | Produced by a range expression with this bound.
    RigidBound String
  | -- | Mismatch in branches.
    RigidCond StructType StructType
  | -- | Invented during unification.
    RigidUnify
  | RigidOutOfScope SrcLoc VName
  | -- | Blank dimension in coercion.
    RigidCoerce
  deriving (RigidSource -> RigidSource -> Bool
(RigidSource -> RigidSource -> Bool)
-> (RigidSource -> RigidSource -> Bool) -> Eq RigidSource
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: RigidSource -> RigidSource -> Bool
$c/= :: RigidSource -> RigidSource -> Bool
== :: RigidSource -> RigidSource -> Bool
$c== :: 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
min :: RigidSource -> RigidSource -> RigidSource
$cmin :: RigidSource -> RigidSource -> RigidSource
max :: RigidSource -> RigidSource -> RigidSource
$cmax :: RigidSource -> RigidSource -> RigidSource
>= :: RigidSource -> RigidSource -> Bool
$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
compare :: RigidSource -> RigidSource -> Ordering
$ccompare :: RigidSource -> RigidSource -> Ordering
$cp1Ord :: Eq 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
showList :: [RigidSource] -> ShowS
$cshowList :: [RigidSource] -> ShowS
show :: RigidSource -> String
$cshow :: RigidSource -> String
showsPrec :: Int -> RigidSource -> ShowS
$cshowsPrec :: Int -> 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
/= :: Rigidity -> Rigidity -> Bool
$c/= :: Rigidity -> Rigidity -> Bool
== :: Rigidity -> Rigidity -> Bool
$c== :: 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
min :: Rigidity -> Rigidity -> Rigidity
$cmin :: Rigidity -> Rigidity -> Rigidity
max :: Rigidity -> Rigidity -> Rigidity
$cmax :: Rigidity -> Rigidity -> Rigidity
>= :: Rigidity -> Rigidity -> Bool
$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
compare :: Rigidity -> Rigidity -> Ordering
$ccompare :: Rigidity -> Rigidity -> Ordering
$cp1Ord :: Eq 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
showList :: [Rigidity] -> ShowS
$cshowList :: [Rigidity] -> ShowS
show :: Rigidity -> String
$cshow :: Rigidity -> String
showsPrec :: Int -> Rigidity -> ShowS
$cshowsPrec :: Int -> Rigidity -> ShowS
Show)

prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource :: SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet Maybe (QualName VName)
Nothing) =
  Doc
"is unknown size returned by function at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidRet (Just QualName VName
fname)) =
  Doc
"is unknown size returned by"
    Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
fname)
    Doc -> Doc -> Doc
<+> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidArg Maybe (QualName VName)
fname String
arg) =
  Doc
"is value of argument"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
arg)
    Doc -> Doc -> Doc
</> Doc
"passed to"
    Doc -> Doc -> Doc
<+> Doc
fname'
    Doc -> Doc -> Doc
<+> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
  where
    fname' :: Doc
fname' = Doc -> (QualName VName -> Doc) -> Maybe (QualName VName) -> Doc
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Doc
"function" (Doc -> Doc
pquote (Doc -> Doc) -> (QualName VName -> Doc) -> QualName VName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr) Maybe (QualName VName)
fname
prettySource SrcLoc
ctx SrcLoc
loc (RigidSlice Maybe Size
d String
slice) =
  Doc
"is size produced by slice"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
slice)
    Doc -> Doc -> Doc
</> Doc
d_desc Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
  where
    d_desc :: Doc
d_desc = case Maybe Size
d of
      Just Size
d' -> Doc
"of dimension of size " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d') Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" "
      Maybe Size
Nothing -> Doc
forall a. Monoid a => a
mempty
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidLoop =
  Doc
"is unknown size of value returned at" Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidRange =
  Doc
"is unknown length of range at" Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidBound String
bound) =
  Doc
"generated from expression"
    Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (String -> Doc
forall a. Pretty a => a -> Doc
shorten String
bound)
    Doc -> Doc -> Doc
</> Doc
"used in range at " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc (RigidOutOfScope SrcLoc
boundloc VName
v) =
  Doc
"is an unknown size arising from "
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName 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
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Doc -> Doc -> Doc
</> Doc
"Originally bound at "
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
boundloc)
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
ctx SrcLoc
loc RigidSource
RigidCoerce =
  Doc
"is an unknown size arising from empty dimension in coercion at"
    Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
prettySource SrcLoc
_ SrcLoc
_ RigidSource
RigidUnify =
  Doc
"is an artificial size invented during unification of functions with anonymous sizes."
prettySource SrcLoc
ctx SrcLoc
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
text (SrcLoc -> SrcLoc -> String
forall a b. (Located a, Located b) => a -> b -> String
locStrRel SrcLoc
ctx SrcLoc
loc)
    Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Doc -> Doc -> Doc
</> Doc
"One branch returns array of type: "
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
    Doc -> Doc -> Doc
</> Doc
"The other an array of type:       "
      Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc -> Doc
align (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr 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 -> Size -> m Notes
dimNotes :: a -> Size -> m Notes
dimNotes a
ctx (NamedSize QualName VName
d) = 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
_, UnknowableSize SrcLoc
loc RigidSource
rsrc) ->
      Notes -> m Notes
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
. String -> Notes
forall a. Pretty a => a -> Notes
aNote (String -> Notes) -> (Doc -> String) -> Doc -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Doc -> String
forall a. Pretty a => a -> String
pretty (Doc -> m Notes) -> Doc -> m Notes
forall a b. (a -> b) -> a -> b
$
        Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
d) Doc -> Doc -> Doc
<+> SrcLoc -> SrcLoc -> RigidSource -> Doc
prettySource (a -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf a
ctx) SrcLoc
loc RigidSource
rsrc
    Maybe (Int, Constraint)
_ -> Notes -> m Notes
forall (f :: * -> *) a. Applicative f => a -> f a
pure Notes
forall a. Monoid a => a
mempty
dimNotes a
_ Size
_ = Notes -> m Notes
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 :: a -> StructType -> m Notes
typeNotes a
ctx =
  ([Notes] -> Notes) -> m [Notes] -> m Notes
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)
mapM (a -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes a
ctx (Size -> m Notes) -> (VName -> Size) -> VName -> m Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. QualName VName -> Size
NamedSize (QualName VName -> Size)
-> (VName -> QualName VName) -> VName -> Size
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
. StructType -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType

typeVarNotes :: MonadUnify m => VName -> m Notes
typeVarNotes :: 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 (Doc -> Notes
forall a. Pretty a => a -> Notes
aNote (Doc -> Notes)
-> ((Int, Constraint) -> Doc) -> (Int, Constraint) -> Notes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Constraint -> Doc
note (Constraint -> Doc)
-> ((Int, Constraint) -> Constraint) -> (Int, Constraint) -> Doc
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 -> Doc
note (HasConstrs Map Name [StructType]
cs Usage
_) =
      VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v
        Doc -> Doc -> Doc
<+> Doc
"="
        Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (((Name, [StructType]) -> Doc) -> [(Name, [StructType])] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, [StructType]) -> Doc
forall a b. Pretty a => (a, b) -> Doc
ppConstr (Map Name [StructType] -> [(Name, [StructType])]
forall k a. Map k a -> [(k, a)]
M.toList Map Name [StructType]
cs))
        Doc -> Doc -> Doc
<+> Doc
"..."
    note (Overloaded [PrimType]
ts Usage
_) =
      VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v Doc -> Doc -> Doc
<+> Doc
"must be one of" Doc -> Doc -> Doc
<+> [Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts))
    note (HasFields Map Name StructType
fs Usage
_) =
      VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
v
        Doc -> Doc -> Doc
<+> Doc
"="
        Doc -> Doc -> Doc
<+> Doc -> Doc
braces ([Doc] -> Doc
forall a. Monoid a => [a] -> a
mconcat (Doc -> [Doc] -> [Doc]
punctuate Doc
", " (((Name, StructType) -> Doc) -> [(Name, StructType)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Name, StructType) -> Doc
forall v b. IsName v => (v, b) -> Doc
ppField (Map Name StructType -> [(Name, StructType)]
forall k a. Map k a -> [(k, a)]
M.toList Map Name StructType
fs))))
    note Constraint
_ = Doc
forall a. Monoid a => a
mempty

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

-- | 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 => SrcLoc -> Name -> m (TypeBase dim als)
  newDimVar :: SrcLoc -> Rigidity -> Name -> m VName

  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 :: a -> m a
normTypeFully a
t = do
  Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  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 :: StructType -> m StructType
normType t :: StructType
t@(Scalar (TypeVar ()
_ Uniqueness
_ (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 (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t
normType StructType
t = StructType -> m StructType
forall (f :: * -> *) a. Applicative f => a -> f a
pure StructType
t

-- | Replace any top-level type variable with its substitution.
normPatType :: MonadUnify m => PatType -> m PatType
normPatType :: PatType -> m PatType
normPatType t :: PatType
t@(Scalar (TypeVar Aliasing
als Uniqueness
u (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
_) ->
      PatType -> m PatType
forall (m :: * -> *). MonadUnify m => PatType -> m PatType
normPatType (PatType -> m PatType) -> PatType -> m PatType
forall a b. (a -> b) -> a -> b
$ StructType
t' StructType -> Uniqueness -> StructType
forall dim as. TypeBase dim as -> Uniqueness -> TypeBase dim as
`setUniqueness` Uniqueness
u StructType -> Aliasing -> PatType
forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` Aliasing
als
    Maybe Constraint
_ -> PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t
normPatType PatType
t = PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t

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

-- | Instantiate existential context in return type.
instantiateEmptyArrayDims ::
  MonadUnify m =>
  SrcLoc ->
  Rigidity ->
  RetTypeBase Size als ->
  m (TypeBase Size als, [VName])
instantiateEmptyArrayDims :: SrcLoc
-> Rigidity
-> RetTypeBase Size als
-> m (TypeBase Size als, [VName])
instantiateEmptyArrayDims SrcLoc
tloc Rigidity
r (RetType [VName]
dims TypeBase Size als
t) = do
  [VName]
dims' <- (VName -> m VName) -> [VName] -> m [VName]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
mapM VName -> m VName
new [VName]
dims
  (TypeBase Size als, [VName]) -> m (TypeBase Size als, [VName])
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((Size -> Size) -> TypeBase Size als -> TypeBase Size als
forall (p :: * -> * -> *) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first ([(VName, VName)] -> Size -> Size
onDim ([(VName, VName)] -> Size -> Size)
-> [(VName, VName)] -> Size -> Size
forall a b. (a -> b) -> a -> b
$ [VName] -> [VName] -> [(VName, VName)]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
dims [VName]
dims') TypeBase Size als
t, [VName]
dims')
  where
    new :: VName -> m VName
new = SrcLoc -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
tloc Rigidity
r (Name -> m VName) -> (VName -> Name) -> VName -> m VName
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Name
nameFromString (String -> Name) -> (VName -> String) -> VName -> Name
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Char -> Bool) -> ShowS
forall a. (a -> Bool) -> [a] -> [a]
takeWhile Char -> Bool
isAscii ShowS -> (VName -> String) -> VName -> String
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> String
baseString
    onDim :: [(VName, VName)] -> Size -> Size
onDim [(VName, VName)]
dims' (NamedSize QualName VName
d) =
      QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ QualName VName
-> (VName -> QualName VName) -> Maybe VName -> QualName VName
forall b a. b -> (a -> b) -> Maybe a -> b
maybe QualName VName
d VName -> QualName VName
forall v. v -> QualName v
qualName (VName -> [(VName, VName)] -> Maybe VName
forall a b. Eq a => a -> [(a, b)] -> Maybe b
lookup (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
d) [(VName, VName)]
dims')
    onDim [(VName, VName)]
_ Size
d = Size
d

-- | 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 (f :: * -> *) a. Applicative f => a -> f a
pure Int
lvl

type UnifyDims m =
  BreadCrumbs -> [VName] -> (VName -> Maybe Int) -> Size -> Size -> m ()

flipUnifyDims :: UnifyDims m -> UnifyDims m
flipUnifyDims :: UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t1 Size
t2 =
  UnifyDims m
onDims BreadCrumbs
bcs [VName]
bound VName -> Maybe Int
nonrigid Size
t2 Size
t1

unifyWith ::
  MonadUnify m =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  StructType ->
  StructType ->
  m ()
unifyWith :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 (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' =
            UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims m
linkDims Usage
usage [VName]
bound BreadCrumbs
bcs
            where
              -- We may have to flip the order of future calls to
              -- onDims inside linkVarToType.
              linkDims :: UnifyDims m
linkDims
                | Bool
ord' = UnifyDims m -> UnifyDims m
forall (m :: * -> *). UnifyDims m -> UnifyDims m
flipUnifyDims UnifyDims m
onDims
                | Bool
otherwise = UnifyDims m
onDims

          unifyTypeArg :: BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs' (TypeArgDim Size
d1 SrcLoc
_) (TypeArgDim Size
d2 SrcLoc
_) =
            BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (Bool -> Size -> Size -> (Size, Size)
forall a. Bool -> a -> a -> (a, a)
swap Bool
ord Size
d1 Size
d2)
          unifyTypeArg BreadCrumbs
bcs' (TypeArgType StructType
t SrcLoc
_) (TypeArgType StructType
arg_t SrcLoc
_) =
            Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
t StructType
arg_t
          unifyTypeArg BreadCrumbs
bcs' TypeArg Size
_ TypeArg Size
_ =
            Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs' (Size
d1, Size
d2) =
            UnifyDims m
onDims
              BreadCrumbs
bcs'
              [VName]
bound
              VName -> Maybe Int
nonrigid
              (TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d1)
              (TypeSubs -> Size -> Size
forall a. Substitutable a => TypeSubs -> a -> a
applySubst (VName -> Constraints -> Maybe (Subst StructRetType)
`lookupSubst` Constraints
constraints) Size
d2)

      case (StructType
t1', StructType
t2') of
        ( 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 ->
                [(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
fs Map Name StructType
arg_fs) (((Name, (StructType, StructType)) -> m ()) -> m ())
-> ((Name, (StructType, StructType)) -> m ()) -> m ()
forall a b. (a -> b) -> a -> b
$ \(Name
k, (StructType
k_t1, StructType
k_t2)) -> do
                  let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb ([Name] -> BreadCrumb
MatchingFields [Name
k]) BreadCrumbs
bcs
                  Bool -> [VName] -> BreadCrumbs -> StructType -> StructType -> m ()
subunify Bool
ord [VName]
bound BreadCrumbs
bcs' StructType
k_t1 StructType
k_t2
            | 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 (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
<+> [Doc] -> Doc
commasep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map Name -> Doc
forall a. Pretty a => a -> Doc
ppr [Name]
missing) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
        ( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
tn) [TypeArg Size]
targs),
          Scalar (TypeVar ()
_ Uniqueness
_ (QualName [VName]
_ VName
arg_tn) [TypeArg Size]
arg_targs)
          )
            | VName
tn VName -> VName -> Bool
forall a. Eq a => a -> a -> Bool
== VName
arg_tn,
              [TypeArg Size] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
targs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [TypeArg Size] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [TypeArg Size]
arg_targs -> do
                let bcs' :: BreadCrumbs
bcs' = BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb (Doc -> BreadCrumb
Matching Doc
"When matching type arguments.") BreadCrumbs
bcs
                (TypeArg Size -> TypeArg Size -> m ())
-> [TypeArg Size] -> [TypeArg Size] -> m ()
forall (m :: * -> *) a b c.
Applicative m =>
(a -> b -> m c) -> [a] -> [b] -> m ()
zipWithM_ (BreadCrumbs -> TypeArg Size -> TypeArg Size -> m ()
unifyTypeArg BreadCrumbs
bcs') [TypeArg Size]
targs [TypeArg Size]
arg_targs
        ( Scalar (TypeVar ()
_ Uniqueness
_ (QualName [] VName
v1) []),
          Scalar (TypeVar ()
_ Uniqueness
_ (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 ()
_ Uniqueness
_ (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 ()
_ Uniqueness
_ (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 ()
_ PName
p1 StructType
a1 (RetType [VName]
b1_dims StructType
b1)),
          Scalar (Arrow ()
_ PName
p2 StructType
a2 (RetType [VName]
b2_dims StructType
b2))
          ) -> 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 Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
forall a. Monoid a => a
mempty)
                    (SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
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] -> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b1_dims ([(Int, Constraint)] -> [(VName, (Int, Constraint))])
-> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> a -> b
$ (Int, Constraint) -> [(Int, Constraint)]
forall a. a -> [a]
repeat (Int
lvl, Constraint
r1)) Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<>)
            (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] -> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. [a] -> [b] -> [(a, b)]
zip [VName]
b2_dims ([(Int, Constraint)] -> [(VName, (Int, Constraint))])
-> [(Int, Constraint)] -> [(VName, (Int, Constraint))]
forall a b. (a -> b) -> a -> b
$ (Int, Constraint) -> [(Int, Constraint)]
forall a. a -> [a]
repeat (Int
lvl, Constraint
r2)) Constraints -> Constraints -> Constraints
forall a. Semigroup a => a -> a -> a
<>)

            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)
              StructType
b1'
              StructType
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 (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
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
              (StructType
b1', StructType
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
$ Size -> Subst t
forall t. Size -> Subst t
SizeSubst (Size -> Subst t) -> Size -> Subst t
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
p1'
                          | Bool
otherwise = Maybe (Subst t)
forall a. Maybe a
Nothing
                     in (StructType
b1, TypeSubs -> StructType -> StructType
forall a. Substitutable a => TypeSubs -> a -> a
applySubst TypeSubs
forall t. VName -> Maybe (Subst t)
f StructType
b2)
                  (PName
_, PName
_) ->
                    (StructType
b1, StructType
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 (Size
t1_d : [Size]
_) <- StructType -> Shape Size
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t1',
            Shape (Size
t2_d : [Size]
_) <- StructType -> Shape Size
forall dim as. TypeBase dim as -> Shape dim
arrayShape StructType
t2',
            Just StructType
t1'' <- Int -> StructType -> Maybe StructType
forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t1',
            Just StructType
t2'' <- Int -> StructType -> Maybe StructType
forall dim as. Int -> TypeBase dim as -> Maybe (TypeBase dim as)
peelArray Int
1 StructType
t2' -> do
              BreadCrumbs -> (Size, Size) -> m ()
onDims' BreadCrumbs
bcs (Bool -> Size -> Size -> (Size, Size)
forall a. Bool -> a -> a -> (a, a)
swap Bool
ord Size
t1_d Size
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 ->
                UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
cs Map Name [StructType]
arg_cs
            | 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_cs) (Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
cs)
                        [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]
cs) (Map Name [StructType] -> [Name]
forall k a. Map k a -> [k]
M.keys Map Name [StructType]
arg_cs)
                Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 constructors:" Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((Name -> Doc) -> [Name] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map ((Doc
"#" Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<>) (Doc -> Doc) -> (Name -> Doc) -> Name -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> Doc
forall a. Pretty a => a -> Doc
ppr) [Name]
missing) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
        (StructType, StructType)
_
          | StructType
t1' StructType -> StructType -> Bool
forall a. Eq a => a -> a -> Bool
== StructType
t2' -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
          | Bool
otherwise -> m ()
forall a. m a
failure

unifyDims :: MonadUnify m => Usage -> UnifyDims m
unifyDims :: Usage -> UnifyDims m
unifyDims Usage
_ BreadCrumbs
_ [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2
  | Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
  | Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1 =
      Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
  | Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2 =
      Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
unifyDims Usage
usage BreadCrumbs
bcs [VName]
_ VName -> Maybe Int
_ Size
d1 Size
d2 = 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 -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 m (Notes -> Notes) -> m Notes -> m Notes
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Usage -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
  Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
"Dimensions"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d1)
      Doc -> Doc -> Doc
<+> Doc
"and"
      Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d2)
      Doc -> Doc -> Doc
<+> Doc
"do not match."

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

-- | @expect super sub@ checks that @sub@ is a subtype of @super@.
expect :: MonadUnify m => Usage -> StructType -> StructType -> m ()
expect :: Usage -> StructType -> StructType -> m ()
expect Usage
usage = UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
forall (f :: * -> *) (t :: * -> *).
(Foldable t, MonadUnify f) =>
BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims Usage
usage [VName]
forall a. Monoid a => a
mempty BreadCrumbs
noBreadCrumbs
  where
    onDims :: BreadCrumbs
-> t VName -> (VName -> Maybe Int) -> Size -> Size -> f ()
onDims BreadCrumbs
_ t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2
      | Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = () -> f ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
    -- We identify existentially bound names by them being nonrigid
    -- and yet bound.  It's OK to unify with those.
    onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid (NamedSize (QualName [VName]
_ VName
d1)) Size
d2
      | Just Int
lvl1 <- VName -> Maybe Int
nonrigid VName
d1,
        Bool -> Bool
not (t VName -> Size -> Bool
forall (t :: * -> *). Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d2) Bool -> Bool -> Bool
|| (VName
d1 VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
          Usage -> BreadCrumbs -> VName -> Int -> Size -> f ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d1 Int
lvl1 Size
d2
    onDims BreadCrumbs
bcs t VName
bound VName -> Maybe Int
nonrigid Size
d1 (NamedSize (QualName [VName]
_ VName
d2))
      | Just Int
lvl2 <- VName -> Maybe Int
nonrigid VName
d2,
        Bool -> Bool
not (t VName -> Size -> Bool
forall (t :: * -> *). Foldable t => t VName -> Size -> Bool
boundParam t VName
bound Size
d1) Bool -> Bool -> Bool
|| (VName
d2 VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound) =
          Usage -> BreadCrumbs -> VName -> Int -> Size -> f ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> BreadCrumbs -> VName -> Int -> Size -> m ()
linkVarToDim Usage
usage BreadCrumbs
bcs VName
d2 Int
lvl2 Size
d1
    onDims BreadCrumbs
bcs t VName
_ VName -> Maybe Int
_ Size
d1 Size
d2 = do
      Notes
notes <- Notes -> Notes -> Notes
forall a. Semigroup a => a -> a -> a
(<>) (Notes -> Notes -> Notes) -> f Notes -> f (Notes -> Notes)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Usage -> Size -> f Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d1 f (Notes -> Notes) -> f Notes -> f Notes
forall (f :: * -> *) a b. Applicative f => f (a -> b) -> f a -> f b
<*> Usage -> Size -> f Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
d2
      Usage -> Notes -> BreadCrumbs -> Doc -> f ()
forall (m :: * -> *) loc a.
(MonadUnify m, Located loc) =>
loc -> Notes -> BreadCrumbs -> Doc -> m a
unifyError Usage
usage Notes
notes BreadCrumbs
bcs (Doc -> f ()) -> Doc -> f ()
forall a b. (a -> b) -> a -> b
$
        Doc
"Dimensions"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d1)
          Doc -> Doc -> Doc
<+> Doc
"and"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Size -> Doc
forall a. Pretty a => a -> Doc
ppr Size
d2)
          Doc -> Doc -> Doc
<+> Doc
"do not match."

    boundParam :: t VName -> Size -> Bool
boundParam t VName
bound (NamedSize (QualName [VName]
_ VName
d)) = VName
d VName -> t VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` t VName
bound
    boundParam t VName
_ Size
_ = Bool
False

occursCheck ::
  MonadUnify m =>
  Usage ->
  BreadCrumbs ->
  VName ->
  StructType ->
  m ()
occursCheck :: 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 as dim. Monoid 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 (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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
        Doc -> Doc -> Doc
<+> Doc
"with"
        Doc -> Doc -> Doc
<+> StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."

scopeCheck ::
  MonadUnify m =>
  Usage ->
  BreadCrumbs ->
  VName ->
  Level ->
  StructType ->
  m ()
scopeCheck :: 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 :: * -> *) as.
(MonadUnify m, Monoid as) =>
Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints StructType
tp
  where
    checkType :: Constraints -> TypeBase Size as -> m ()
checkType Constraints
constraints TypeBase Size as
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 Size as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase Size as
t Set VName -> Set VName -> Set VName
forall a. Semigroup a => a -> a -> a
<> TypeBase Size as -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType TypeBase Size as
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 (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 (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
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
          Doc -> Doc -> Doc
</> Doc
"with"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
          Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
          Doc -> Doc -> Doc
</> Doc
"This is because"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (v -> Doc
forall v. IsName v => v -> Doc
pprName v
v)
          Doc -> Doc -> Doc
<+> Doc
"is rigidly bound in a deeper scope."

linkVarToType ::
  MonadUnify m =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  VName ->
  Level ->
  StructType ->
  m ()
linkVarToType :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> VName
-> Int
-> StructType
-> m ()
linkVarToType UnifyDims 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

  Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  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
            ext :: [VName]
ext = (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter VName -> Bool
used [VName]
bound
        case (VName -> Bool) -> [VName] -> [VName]
forall a. (a -> Bool) -> [a] -> [a]
filter (VName -> Set VName -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`notElem` Set VName
witnessed) [VName]
ext of
          [] ->
            (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)
          [VName]
problems ->
            Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
withIndexLink Doc
"unify-param-existential" (Doc -> m ()) -> Doc -> m ()
forall a b. (a -> b) -> a -> b
$
              Doc
"Parameter(s) "
                Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
commasep ((VName -> Doc) -> [VName] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (Doc -> Doc
pquote (Doc -> Doc) -> (VName -> Doc) -> VName -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VName -> Doc
forall v. IsName v => v -> Doc
pprName) [VName]
problems)
                Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
" used as size(s) would go out of scope."

  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
      let bcs' :: BreadCrumbs
bcs' =
            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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
                    Doc -> Doc -> Doc
<+> String -> Doc
textwrap String
"is not instantiated with a function type, due to"
                    Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
unlift_usage
              )
              BreadCrumbs
bcs

      m ()
link

      Usage -> BreadCrumbs -> StructType -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs' 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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [VName]
bound) (StructType -> Set VName
forall as. TypeBase Size as -> Set VName
freeInType StructType
tp)) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
        Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
            Doc -> Doc -> Doc
<+> Doc
"cannot be instantiated with type containing anonymous sizes:"
            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
            Doc -> Doc -> Doc
</> String -> Doc
textwrap String
"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 as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> 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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> (PrimType -> ScalarTypeBase Size ()) -> PrimType -> StructType
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PrimType -> ScalarTypeBase Size ()
forall dim as. PrimType -> ScalarTypeBase dim as
Prim) [PrimType]
ts -> do
          m ()
link
          case StructType
tp of
            Scalar (TypeVar ()
_ Uniqueness
_ (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 (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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"with type"
                  Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
                  Doc -> Doc -> Doc
</> Doc
"as"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"must be one of"
                  Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
                  Doc -> Doc -> Doc
<+/> Doc
"due to"
                  Doc -> Doc -> Doc
<+/> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Just (HasFields Map Name StructType
required_fields Usage
old_usage) -> do
      m ()
link
      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)
mapM StructType -> m StructType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully Map Name StructType
required_fields
              let bcs' :: BreadCrumbs
bcs' =
                    BreadCrumb -> BreadCrumbs -> BreadCrumbs
breadCrumb
                      ( Doc -> BreadCrumb
Matching (Doc -> BreadCrumb) -> Doc -> BreadCrumb
forall a b. (a -> b) -> a -> b
$
                          VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn
                            Doc -> Doc -> Doc
<+> Doc
"must be a record with at least the fields:"
                            Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (ScalarTypeBase Size () -> Doc
forall a. Pretty a => a -> Doc
ppr (Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields'))
                            Doc -> Doc -> Doc
</> Doc
"due to"
                            Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
                      )
                      BreadCrumbs
bcs
              ((StructType, StructType) -> m ())
-> [(StructType, StructType)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((StructType -> StructType -> m ())
-> (StructType, StructType) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry ((StructType -> StructType -> m ())
 -> (StructType, StructType) -> m ())
-> (StructType -> StructType -> m ())
-> (StructType, StructType)
-> m ()
forall a b. (a -> b) -> a -> b
$ UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') ([(StructType, StructType)] -> m ())
-> [(StructType, StructType)] -> m ()
forall a b. (a -> b) -> a -> b
$
                Map Name (StructType, StructType) -> [(StructType, StructType)]
forall k a. Map k a -> [a]
M.elems (Map Name (StructType, StructType) -> [(StructType, StructType)])
-> Map Name (StructType, StructType) -> [(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
required_fields Map Name StructType
tp_fields
        Scalar (TypeVar ()
_ Uniqueness
_ (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 ->
              (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
lvl, Map Name StructType -> Usage -> Constraint
HasFields Map Name StructType
required_fields Usage
old_usage)
        StructType
_ ->
          Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"with type"
              Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
tp)
              Doc -> Doc -> Doc
</> Doc
"as"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"must be a record with fields"
              Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (ScalarTypeBase Size () -> Doc
forall a. Pretty a => a -> Doc
ppr (Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record Map Name StructType
required_fields))
              Doc -> Doc -> Doc
</> Doc
"due to"
              Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
old_usage Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    -- See Note [Linking variables to sum types]
    Just (HasConstrs Map Name [StructType]
required_cs Usage
old_usage) ->
      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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Size ()
forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum (Map Name [StructType] -> ScalarTypeBase Size ())
-> Map Name [StructType] -> ScalarTypeBase Size ()
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` StructType -> Set VName
forall as. TypeBase Size as -> Set VName
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)
              UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
ts
        Scalar (TypeVar ()
_ Uniqueness
_ (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 Map Name [StructType]
v_cs Usage
_) -> do
              UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Map Name [StructType]
required_cs Map Name [StructType]
v_cs
            Just (Int
_, NoConstraint {}) -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
            Just (Int
_, Equality {}) -> () -> m ()
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 (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, Map Name [StructType] -> Usage -> Constraint
HasConstrs Map Name [StructType]
required_cs Usage
old_usage)
          where
            combineConstrs :: (Int, Constraint) -> (a, Constraint) -> (Int, Constraint)
combineConstrs (Int
_, HasConstrs Map Name [StructType]
cs1 Usage
usage1) (a
_, HasConstrs Map Name [StructType]
cs2 Usage
_) =
              (Int
lvl, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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
forall a. Monoid a => a
mempty
    Maybe Constraint
_ -> m ()
link
  where
    noSumType :: Notes -> m a
noSumType Notes
notes =
      Usage -> 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"

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

  case Size
dim of
    NamedSize QualName VName
dim'
      | Just (Int
dim_lvl, Constraint
c) <- QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName 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 -> Size -> m Notes
forall a (m :: * -> *).
(Located a, MonadUnify m) =>
a -> Size -> m Notes
dimNotes Usage
usage Size
dim
              Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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 unify size variable"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
                  Doc -> Doc -> Doc
<+> Doc
"with"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"(scope violation)."
                  Doc -> Doc -> Doc
</> Doc
"This is because"
                  Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (QualName VName -> Doc
forall a. Pretty a => a -> Doc
ppr QualName VName
dim')
                  Doc -> Doc -> Doc
<+> Doc
"is rigidly bound in a deeper scope."
            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 (QualName VName -> VName
forall vn. QualName vn -> vn
qualLeaf QualName VName
dim') (Int
lvl, Constraint
c)
    Size
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

  (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 Size -> Usage -> Constraint
Size (Size -> Maybe Size
forall a. a -> Maybe a
Just Size
dim) Usage
usage)

-- | Assert that this type must be one of the given primitive types.
mustBeOneOf :: MonadUnify m => [PrimType] -> Usage -> StructType -> m ()
mustBeOneOf :: [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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (PrimType -> ScalarTypeBase Size ()
forall dim as. PrimType -> ScalarTypeBase dim as
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 ()
_ Uniqueness
_ (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 (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [PrimType]
ts -> () -> m ()
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 (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
$
        String -> Doc
text String
"Cannot unify type"
          Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t)
          Doc -> Doc -> Doc
<+> Doc
"with any of " Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."

linkVarToTypes :: MonadUnify m => Usage -> VName -> [PrimType] -> m ()
linkVarToTypes :: 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]
`intersect` [PrimType]
vn_ts of
        [] ->
          Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
              Doc -> Doc -> Doc
<+> Doc
"but also one of"
              Doc -> Doc -> Doc
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
vn_ts)
              Doc -> Doc -> Doc
<+> Doc
"due to"
              Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr 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 Map Name [StructType]
_ Usage
vn_usage) ->
      Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [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
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
vn_usage
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    Just (Int
_, HasFields Map Name StructType
_ Usage
vn_usage) ->
      Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)
            Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
", but also inferred to be record due to"
          Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr 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 (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
<+> [Doc] -> Doc
commasep ((PrimType -> Doc) -> [PrimType] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map PrimType -> Doc
forall a. Pretty a => a -> Doc
ppr [PrimType]
ts)

-- | Assert that this type must support equality.
equalityType ::
  (MonadUnify m, Pretty (Shape dim), Monoid as) =>
  Usage ->
  TypeBase dim as ->
  m ()
equalityType :: Usage -> TypeBase dim as -> m ()
equalityType Usage
usage TypeBase dim as
t = do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
<+> Doc
"does not support equality (is higher-order)."
  (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 as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars TypeBase dim as
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 ()
_ Uniqueness
_ (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 (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
<+> Doc -> Doc
pquote (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t)
                  Doc -> Doc -> Doc
<+> Doc
"does not support equality."
                  Doc -> Doc -> Doc
</> Doc
"Constrained to be higher-order due to"
                  Doc -> Doc -> Doc
<+> Usage -> Doc
forall a. Pretty a => a -> Doc
ppr Usage
cusage
                  Doc -> Doc -> Doc
<+> Doc
"."
          | Bool
otherwise -> () -> m ()
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 (f :: * -> *) a. Applicative f => a -> f a
pure () -- All primtypes support equality.
        Just (Int
_, Equality {}) ->
          () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        Just (Int
_, HasConstrs Map Name [StructType]
cs Usage
_) ->
          (StructType -> m ()) -> [StructType] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (Usage -> StructType -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> TypeBase dim as -> m ()
equalityType Usage
usage) ([StructType] -> m ()) -> [StructType] -> m ()
forall a b. (a -> b) -> a -> b
$ [[StructType]] -> [StructType]
forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat ([[StructType]] -> [StructType]) -> [[StructType]] -> [StructType]
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> [[StructType]]
forall k a. Map k a -> [a]
M.elems Map Name [StructType]
cs
        Maybe (Int, Constraint)
_ ->
          Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn Doc -> Doc -> Doc
<+> Doc
"does not support equality."

zeroOrderTypeWith ::
  (MonadUnify m, Pretty (Shape dim), Monoid as) =>
  Usage ->
  BreadCrumbs ->
  TypeBase dim as ->
  m ()
zeroOrderTypeWith :: Usage -> BreadCrumbs -> TypeBase dim as -> m ()
zeroOrderTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
</> Int -> Doc -> Doc
indent Int
2 (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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 as -> [VName]) -> TypeBase dim as -> 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 as -> Set VName) -> TypeBase dim as -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars (TypeBase dim as -> m ()) -> TypeBase dim as -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim as
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
Lifted SrcLoc
ploc) ->
          Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
              Doc -> Doc -> Doc
<+> Doc
"at"
              Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
ploc)
              Doc -> Doc -> Doc
<+> Doc
"may be a function."
        Maybe (Int, Constraint)
_ -> () -> m ()
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()

-- | Assert that this type must be zero-order.
zeroOrderType ::
  (MonadUnify m, Pretty (Shape dim), Monoid as) =>
  Usage ->
  String ->
  TypeBase dim as ->
  m ()
zeroOrderType :: Usage -> String -> TypeBase dim as -> m ()
zeroOrderType Usage
usage String
desc =
  Usage -> BreadCrumbs -> TypeBase dim as -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
zeroOrderTypeWith Usage
usage (BreadCrumbs -> TypeBase dim as -> m ())
-> BreadCrumbs -> TypeBase dim as -> 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
<+> String -> Doc
textwrap String
desc

arrayElemTypeWith ::
  (MonadUnify m, Pretty (Shape dim), Monoid as) =>
  Usage ->
  BreadCrumbs ->
  TypeBase dim as ->
  m ()
arrayElemTypeWith :: Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage BreadCrumbs
bcs TypeBase dim as
t = do
  Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (TypeBase dim as -> Bool
forall dim as. TypeBase dim as -> Bool
orderZero TypeBase dim as
t) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$
    Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
</> Int -> Doc -> Doc
indent Int
2 (TypeBase dim as -> Doc
forall a. Pretty a => a -> Doc
ppr TypeBase dim as
t) Doc -> Doc -> Doc
</> 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 as -> [VName]) -> TypeBase dim as -> 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 as -> Set VName) -> TypeBase dim as -> [VName]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. TypeBase dim as -> Set VName
forall as dim. Monoid as => TypeBase dim as -> Set VName
typeVars (TypeBase dim as -> m ()) -> TypeBase dim as -> m ()
forall a b. (a -> b) -> a -> b
$ TypeBase dim as
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 SrcLoc
ploc)
          | Liftedness
l Liftedness -> [Liftedness] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` [Liftedness
Lifted, Liftedness
SizeLifted] ->
              Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (VName -> Doc
forall v. IsName v => v -> Doc
pprName VName
vn)
                  Doc -> Doc -> Doc
<+> Doc
"bound at"
                  Doc -> Doc -> Doc
<+> String -> Doc
text (SrcLoc -> String
forall a. Located a => a -> String
locStr SrcLoc
ploc)
                  Doc -> Doc -> Doc
<+> Doc
"is lifted and cannot be an array element."
        Maybe (Int, Constraint)
_ -> () -> m ()
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), Monoid as) =>
  Usage ->
  String ->
  TypeBase dim as ->
  m ()
arrayElemType :: Usage -> String -> TypeBase dim as -> m ()
arrayElemType Usage
usage String
desc =
  Usage -> BreadCrumbs -> TypeBase dim as -> m ()
forall (m :: * -> *) dim as.
(MonadUnify m, Pretty (Shape dim), Monoid as) =>
Usage -> BreadCrumbs -> TypeBase dim as -> m ()
arrayElemTypeWith Usage
usage (BreadCrumbs -> TypeBase dim as -> m ())
-> BreadCrumbs -> TypeBase dim as -> 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
<+> String -> Doc
textwrap String
desc

unifySharedConstructors ::
  MonadUnify m =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  M.Map Name [StructType] ->
  M.Map Name [StructType] ->
  m ()
unifySharedConstructors :: UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> Map Name [StructType]
-> Map Name [StructType]
-> m ()
unifySharedConstructors UnifyDims 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 (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
f1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> 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_ (UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs') [StructType]
f1 [StructType]
f2
      | Bool
otherwise =
          Usage -> Notes -> BreadCrumbs -> Doc -> m ()
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
<+> Doc -> Doc
pquote (Name -> Doc
forall v. IsName v => v -> Doc
pprName 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 :: 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 ()
_ Uniqueness
_ (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
          (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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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 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, Map Name [StructType] -> Usage -> Constraint
HasConstrs (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 (t :: * -> *) a. Foldable t => t a -> Int
length [StructType]
fs Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [StructType] -> 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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr 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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> Doc
"not present in type."
        Just [StructType]
fs'
          | [StructType] -> 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 (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 (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
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
c) Doc -> Doc -> Doc
<+> 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 Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name [StructType] -> ScalarTypeBase Size ()
forall dim as. Map Name [TypeBase dim as] -> ScalarTypeBase dim as
Sum (Map Name [StructType] -> ScalarTypeBase Size ())
-> Map Name [StructType] -> ScalarTypeBase Size ()
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 =>
  UnifyDims m ->
  Usage ->
  [VName] ->
  BreadCrumbs ->
  Name ->
  PatType ->
  m PatType
mustHaveFieldWith :: UnifyDims m
-> Usage -> [VName] -> BreadCrumbs -> Name -> PatType -> m PatType
mustHaveFieldWith UnifyDims m
onDims Usage
usage [VName]
bound BreadCrumbs
bcs Name
l PatType
t = do
  Constraints
constraints <- m Constraints
forall (m :: * -> *). MonadUnify m => m Constraints
getConstraints
  StructType
l_type <- SrcLoc -> Name -> m StructType
forall (m :: * -> *) als dim.
(MonadUnify m, Monoid als) =>
SrcLoc -> Name -> m (TypeBase dim als)
newTypeVar (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) Name
"t"
  let l_type' :: PatType
l_type' = StructType
l_type StructType -> Aliasing -> PatType
forall dim asf ast. TypeBase dim asf -> ast -> TypeBase dim ast
`setAliases` PatType -> Aliasing
forall as shape. Monoid as => TypeBase shape as -> as
aliases PatType
t
  case PatType
t of
    Scalar (TypeVar Aliasing
_ Uniqueness
_ (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, Map Name StructType -> Usage -> Constraint
HasFields (Name -> StructType -> Map Name StructType
forall k a. k -> a -> Map k a
M.singleton Name
l StructType
l_type) Usage
usage)
          PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
      | Just (Int
lvl, HasFields 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' -> UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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, Map Name StructType -> Usage -> Constraint
HasFields (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)
          PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'
    Scalar (Record Map Name PatType
fields)
      | Just PatType
t' <- Name -> Map Name PatType -> Maybe PatType
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
l Map Name PatType
fields -> do
          Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage StructType
l_type (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t'
          PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
t'
      | Bool
otherwise ->
          Usage -> Notes -> BreadCrumbs -> Doc -> m PatType
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 PatType) -> Doc -> m PatType
forall a b. (a -> b) -> a -> b
$
            Doc
"Attempt to access field"
              Doc -> Doc -> Doc
<+> Doc -> Doc
pquote (Name -> Doc
forall a. Pretty a => a -> Doc
ppr Name
l)
              Doc -> Doc -> Doc
<+> Doc
" of value of type"
              Doc -> Doc -> Doc
<+> TypeBase () () -> Doc
forall a. Pretty a => a -> Doc
ppr (PatType -> TypeBase () ()
forall dim as. TypeBase dim as -> TypeBase () ()
toStructural PatType
t) Doc -> Doc -> Doc
forall a. Semigroup a => a -> a -> a
<> Doc
"."
    PatType
_ -> do
      Usage -> StructType -> StructType -> m ()
forall (m :: * -> *).
MonadUnify m =>
Usage -> StructType -> StructType -> m ()
unify Usage
usage (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t) (StructType -> m ()) -> StructType -> m ()
forall a b. (a -> b) -> a -> b
$ ScalarTypeBase Size () -> StructType
forall dim as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase Size () -> StructType)
-> ScalarTypeBase Size () -> StructType
forall a b. (a -> b) -> a -> b
$ Map Name StructType -> ScalarTypeBase Size ()
forall dim as. Map Name (TypeBase dim as) -> ScalarTypeBase dim as
Record (Map Name StructType -> ScalarTypeBase Size ())
-> Map Name StructType -> ScalarTypeBase Size ()
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
      PatType -> m PatType
forall (f :: * -> *) a. Applicative f => a -> f a
pure PatType
l_type'

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

newDimOnMismatch ::
  (Monoid as, MonadUnify m) =>
  SrcLoc ->
  TypeBase Size as ->
  TypeBase Size as ->
  m (TypeBase Size as, [VName])
newDimOnMismatch :: SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch SrcLoc
loc TypeBase Size as
t1 TypeBase Size as
t2 = do
  (TypeBase Size as
t, Map (Size, Size) VName
seen) <- StateT (Map (Size, Size) VName) m (TypeBase Size as)
-> Map (Size, Size) VName
-> m (TypeBase Size as, Map (Size, Size) VName)
forall s (m :: * -> *) a. StateT s m a -> s -> m (a, s)
runStateT (([VName] -> Size -> Size -> StateT (Map (Size, Size) VName) m Size)
-> TypeBase Size as
-> TypeBase Size as
-> StateT (Map (Size, Size) VName) m (TypeBase Size as)
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] -> Size -> Size -> StateT (Map (Size, Size) VName) m Size
forall (t :: (* -> *) -> * -> *) (m :: * -> *) p.
(MonadState (Map (Size, Size) VName) (t m), MonadTrans t,
 MonadUnify m) =>
p -> Size -> Size -> t m Size
onDims TypeBase Size as
t1 TypeBase Size as
t2) Map (Size, Size) VName
forall a. Monoid a => a
mempty
  (TypeBase Size as, [VName]) -> m (TypeBase Size as, [VName])
forall (f :: * -> *) a. Applicative f => a -> f a
pure (TypeBase Size as
t, Map (Size, Size) VName -> [VName]
forall k a. Map k a -> [a]
M.elems Map (Size, Size) VName
seen)
  where
    r :: Rigidity
r = RigidSource -> Rigidity
Rigid (RigidSource -> Rigidity) -> RigidSource -> Rigidity
forall a b. (a -> b) -> a -> b
$ StructType -> StructType -> RigidSource
RigidCond (TypeBase Size as -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t1) (TypeBase Size as -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct TypeBase Size as
t2)
    onDims :: p -> Size -> Size -> t m Size
onDims p
_ Size
d1 Size
d2
      | Size
d1 Size -> Size -> Bool
forall a. Eq a => a -> a -> Bool
== Size
d2 = Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure Size
d1
      | Bool
otherwise = do
          -- Remember mismatches we have seen before and reuse the
          -- same new size.
          Maybe VName
maybe_d <- (Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName)
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets ((Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName))
-> (Map (Size, Size) VName -> Maybe VName) -> t m (Maybe VName)
forall a b. (a -> b) -> a -> b
$ (Size, Size) -> Map (Size, Size) VName -> Maybe VName
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup (Size
d1, Size
d2)
          case Maybe VName
maybe_d of
            Just VName
d -> Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> t m Size) -> Size -> t m Size
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
d
            Maybe VName
Nothing -> do
              VName
d <- m VName -> t m VName
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 -> Rigidity -> Name -> m VName
forall (m :: * -> *).
MonadUnify m =>
SrcLoc -> Rigidity -> Name -> m VName
newDimVar SrcLoc
loc Rigidity
r Name
"differ"
              (Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ())
-> (Map (Size, Size) VName -> Map (Size, Size) VName) -> t m ()
forall a b. (a -> b) -> a -> b
$ (Size, Size)
-> VName -> Map (Size, Size) VName -> Map (Size, Size) VName
forall k a. Ord k => k -> a -> Map k a -> Map k a
M.insert (Size
d1, Size
d2) VName
d
              Size -> t m Size
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Size -> t m Size) -> Size -> t m Size
forall a b. (a -> b) -> a -> b
$ QualName VName -> Size
NamedSize (QualName VName -> Size) -> QualName VName -> Size
forall a b. (a -> b) -> a -> b
$ VName -> QualName VName
forall v. v -> QualName v
qualName VName
d

-- | Like unification, but creates new size variables where mismatches
-- occur.  Returns the new dimensions thus created.
unifyMostCommon ::
  MonadUnify m =>
  Usage ->
  PatType ->
  PatType ->
  m (PatType, [VName])
unifyMostCommon :: Usage -> PatType -> PatType -> m (PatType, [VName])
unifyMostCommon Usage
usage PatType
t1 PatType
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 (f :: * -> *) a. Applicative f => a -> f a
pure ()
  UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
forall (m :: * -> *).
MonadUnify m =>
UnifyDims m
-> Usage
-> [VName]
-> BreadCrumbs
-> StructType
-> StructType
-> m ()
unifyWith UnifyDims 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 (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t1) (PatType -> StructType
forall dim as. TypeBase dim as -> TypeBase dim ()
toStruct PatType
t2)
  PatType
t1' <- PatType -> m PatType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t1
  PatType
t2' <- PatType -> m PatType
forall a (m :: * -> *). (Substitutable a, MonadUnify m) => a -> m a
normTypeFully PatType
t2
  SrcLoc -> PatType -> PatType -> m (PatType, [VName])
forall as (m :: * -> *).
(Monoid as, MonadUnify m) =>
SrcLoc
-> TypeBase Size as
-> TypeBase Size as
-> m (TypeBase Size as, [VName])
newDimOnMismatch (Usage -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf Usage
usage) PatType
t1' PatType
t2'

-- Simple MonadUnify implementation.

type UnifyMState = (Constraints, Int)

newtype UnifyM a = UnifyM (StateT UnifyMState (Except TypeError) a)
  deriving
    ( Applicative UnifyM
a -> UnifyM a
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
UnifyM a -> (a -> UnifyM b) -> UnifyM b
UnifyM a -> UnifyM b -> UnifyM b
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
return :: a -> UnifyM a
$creturn :: forall a. a -> UnifyM a
>> :: UnifyM a -> UnifyM b -> UnifyM b
$c>> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
>>= :: UnifyM a -> (a -> UnifyM b) -> UnifyM b
$c>>= :: forall a b. UnifyM a -> (a -> UnifyM b) -> UnifyM b
$cp1Monad :: Applicative UnifyM
Monad,
      a -> UnifyM b -> UnifyM a
(a -> b) -> UnifyM a -> UnifyM b
(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
<$ :: a -> UnifyM b -> UnifyM a
$c<$ :: forall a b. a -> UnifyM b -> UnifyM a
fmap :: (a -> b) -> UnifyM a -> UnifyM b
$cfmap :: forall a b. (a -> b) -> UnifyM a -> UnifyM b
Functor,
      Functor UnifyM
a -> UnifyM a
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
UnifyM a -> UnifyM b -> UnifyM b
UnifyM a -> UnifyM b -> UnifyM a
UnifyM (a -> b) -> UnifyM a -> UnifyM b
(a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
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
<* :: UnifyM a -> UnifyM b -> UnifyM a
$c<* :: forall a b. UnifyM a -> UnifyM b -> UnifyM a
*> :: UnifyM a -> UnifyM b -> UnifyM b
$c*> :: forall a b. UnifyM a -> UnifyM b -> UnifyM b
liftA2 :: (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
$cliftA2 :: forall a b c. (a -> b -> c) -> UnifyM a -> UnifyM b -> UnifyM c
<*> :: UnifyM (a -> b) -> UnifyM a -> UnifyM b
$c<*> :: forall a b. UnifyM (a -> b) -> UnifyM a -> UnifyM b
pure :: a -> UnifyM a
$cpure :: forall a. a -> UnifyM a
$cp1Applicative :: Functor UnifyM
Applicative,
      MonadState UnifyMState,
      MonadError TypeError
    )

newVar :: Name -> UnifyM VName
newVar :: Name -> UnifyM VName
newVar Name
name = do
  (Constraints
x, Int
i) <- UnifyM UnifyMState
forall s (m :: * -> *). MonadState s m => m s
get
  UnifyMState -> 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 (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 = (UnifyMState -> Constraints) -> UnifyM Constraints
forall s (m :: * -> *) a. MonadState s m => (s -> a) -> m a
gets UnifyMState -> Constraints
forall a b. (a, b) -> a
fst
  putConstraints :: Constraints -> UnifyM ()
putConstraints Constraints
x = (UnifyMState -> UnifyMState) -> UnifyM ()
forall s (m :: * -> *). MonadState s m => (s -> s) -> m ()
modify ((UnifyMState -> UnifyMState) -> UnifyM ())
-> (UnifyMState -> UnifyMState) -> UnifyM ()
forall a b. (a -> b) -> a -> b
$ \(Constraints
_, Int
i) -> (Constraints
x, Int
i)

  newTypeVar :: SrcLoc -> Name -> UnifyM (TypeBase dim als)
newTypeVar SrcLoc
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 String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc)
    TypeBase dim als -> UnifyM (TypeBase dim als)
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 as. ScalarTypeBase dim as -> TypeBase dim as
Scalar (ScalarTypeBase dim als -> TypeBase dim als)
-> ScalarTypeBase dim als -> TypeBase dim als
forall a b. (a -> b) -> a -> b
$ als
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim als
forall dim as.
as
-> Uniqueness
-> QualName VName
-> [TypeArg dim]
-> ScalarTypeBase dim as
TypeVar als
forall a. Monoid a => a
mempty Uniqueness
Nonunique (VName -> QualName VName
forall v. v -> QualName v
qualName VName
v) []

  newDimVar :: SrcLoc -> Rigidity -> Name -> UnifyM VName
newDimVar SrcLoc
loc 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, SrcLoc -> RigidSource -> Constraint
UnknowableSize SrcLoc
loc 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 Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc)
    VName -> UnifyM VName
forall (f :: * -> *) a. Applicative f => a -> f a
pure VName
dim

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

  unifyError :: loc -> Notes -> BreadCrumbs -> Doc -> UnifyM a
unifyError loc
loc Notes
notes BreadCrumbs
bcs Doc
doc =
    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. Pretty a => a -> Doc
ppr BreadCrumbs
bcs

  matchError :: loc -> Notes -> BreadCrumbs -> StructType -> StructType -> UnifyM a
matchError loc
loc Notes
notes BreadCrumbs
bcs StructType
t1 StructType
t2 =
    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. Pretty a => a -> Doc
ppr BreadCrumbs
bcs
    where
      doc :: Doc
doc =
        Doc
"Types"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t1)
          Doc -> Doc -> Doc
</> Doc
"and"
          Doc -> Doc -> Doc
</> Int -> Doc -> Doc
indent Int
2 (StructType -> Doc
forall a. Pretty a => a -> Doc
ppr StructType
t2)
          Doc -> Doc -> Doc
</> Doc
"do not match."

runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM :: [TypeParam] -> [TypeParam] -> UnifyM a -> Either TypeError a
runUnifyM [TypeParam]
rigid_tparams [TypeParam]
nonrigid_tparams (UnifyM StateT UnifyMState (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 UnifyMState (Except TypeError) a
-> UnifyMState -> Except TypeError a
forall (m :: * -> *) s a. Monad m => StateT s m a -> s -> m a
evalStateT StateT UnifyMState (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
0, Maybe Size -> Usage -> Constraint
Size Maybe Size
forall a. Maybe a
Nothing (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc))
    nonrigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> Usage -> Constraint
NoConstraint Liftedness
l (Usage -> Constraint) -> Usage -> Constraint
forall a b. (a -> b) -> a -> b
$ Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing SrcLoc
loc))
    rigid :: TypeParamBase a -> (a, (a, Constraint))
rigid (TypeParamDim a
p SrcLoc
loc) = (a
p, (a
0, SrcLoc -> Constraint
ParamSize SrcLoc
loc))
    rigid (TypeParamType Liftedness
l a
p SrcLoc
loc) = (a
p, (a
0, Liftedness -> SrcLoc -> Constraint
ParamType Liftedness
l 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 ()
expect (Maybe String -> SrcLoc -> Usage
Usage Maybe String
forall a. Maybe a
Nothing (Loc -> SrcLoc
forall a. Located a => a -> SrcLoc
srclocOf 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.