summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorDougal <d.maclaurin@gmail.com>2023-12-04 21:23:20 -0500
committerDougal <d.maclaurin@gmail.com>2023-12-04 21:23:20 -0500
commitd10e03cc91e4578cefe75e74e572fd4e2f95ab6c (patch)
treeafb0672cab5a2ae07450f2a3984374d8d2db4f74
parent6595db0dbd23bb0409229f37e99d7f1709f56c62 (diff)
Start adding SrcIds to user-facing errors
Diffstat
-rw-r--r--src/lib/AbstractSyntax.hs58
-rw-r--r--src/lib/Err.hs9
-rw-r--r--src/lib/Export.hs12
-rw-r--r--src/lib/Inference.hs467
-rw-r--r--src/lib/Lexing.hs2
-rw-r--r--src/lib/Name.hs13
-rw-r--r--src/lib/QueryType.hs5
-rw-r--r--src/lib/Runtime.hs2
-rw-r--r--src/lib/SourceRename.hs137
-rw-r--r--src/lib/TopLevel.hs37
-rw-r--r--src/lib/Types/Source.hs8
11 files changed, 382 insertions, 368 deletions
diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs
index 6a4b2584..e7a396ce 100644
--- a/src/lib/AbstractSyntax.hs
+++ b/src/lib/AbstractSyntax.hs
@@ -139,7 +139,7 @@ decl ann (WithSrcs sid _ d) = WithSrcB sid <$> case d of
CLet binder rhs -> do
(p, ty) <- patOptAnn binder
ULet ann p ty <$> asExpr <$> block rhs
- CBind _ _ -> throw TopLevelArrowBinder
+ CBind _ _ -> throw sid TopLevelArrowBinder
CDefDecl def -> do
(name, lam) <- aDef def
return $ ULet ann (fromSourceNameW name) Nothing (WithSrcE sid (ULam lam))
@@ -199,7 +199,7 @@ withTrailingConstraints g cont = case g of
Nest (UAnnBinder expl (WithSrcB sid b) ann cs) bs <- withTrailingConstraints lhs cont
s <- case b of
UBindSource s -> return s
- UIgnore -> throw CantConstrainAnonBinders
+ UIgnore -> throw sid CantConstrainAnonBinders
UBind _ _ -> error "Shouldn't have internal names until renaming pass"
c' <- expr c
return $ UnaryNest (UAnnBinder expl (WithSrcB sid b) ann (cs ++ [c']))
@@ -261,7 +261,7 @@ uBinder :: GroupW -> SyntaxM (UBinder c VoidS VoidS)
uBinder (WithSrcs sid _ b) = case b of
CLeaf (CIdentifier name) -> return $ fromSourceNameW $ WithSrc sid name
CLeaf CHole -> return $ WithSrcB sid UIgnore
- _ -> throw UnexpectedBinder
+ _ -> throw sid UnexpectedBinder
-- Type annotation with an optional binder pattern
tyOptPat :: GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
@@ -300,7 +300,7 @@ pat (WithSrcs sid _ grp) = WithSrcB sid <$> case grp of
CLeaf (CIdentifier name) -> return $ UPatBinder $ fromSourceNameW $ WithSrc sid name
CJuxtapose True lhs rhs -> do
case lhs of
- WithSrcs _ _ (CJuxtapose True _ _) -> throw OnlyUnaryWithoutParens
+ WithSrcs lhsId _ (CJuxtapose True _ _) -> throw lhsId OnlyUnaryWithoutParens
_ -> return ()
name <- identifier "pattern constructor name" lhs
arg <- pat rhs
@@ -312,11 +312,11 @@ pat (WithSrcs sid _ grp) = WithSrcB sid <$> case grp of
gs' <- mapM pat gs
return $ UPatCon (fromSourceNameW name) (toNest gs')
_ -> error "unexpected postfix group (should be ruled out at grouping stage)"
- _ -> throw IllegalPattern
+ _ -> throw sid IllegalPattern
tyOptBinder :: Explicitness -> GroupW -> SyntaxM (UAnnBinder VoidS VoidS)
tyOptBinder expl (WithSrcs sid sids grp) = case grp of
- CBin (WithSrc _ Pipe) _ _ -> throw UnexpectedConstraint
+ CBin (WithSrc _ Pipe) _ rhs -> throw (getSrcId rhs) UnexpectedConstraint
CBin (WithSrc _ Colon) name ty -> do
b <- uBinder name
ann <- UAnn <$> expr ty
@@ -340,7 +340,7 @@ binderReqTy expl (WithSrcs _ _ (CBin (WithSrc _ Colon) name ty)) = do
b <- uBinder name
ann <- UAnn <$> expr ty
return $ UAnnBinder expl b ann []
-binderReqTy _ _ = throw ExpectedAnnBinder
+binderReqTy _ g = throw (getSrcId g) ExpectedAnnBinder
argList :: [GroupW] -> SyntaxM ([UExpr VoidS], [UNamedArg VoidS])
argList gs = partitionEithers <$> mapM singleArg gs
@@ -354,7 +354,7 @@ singleArg = \case
identifier :: String -> GroupW -> SyntaxM SourceNameW
identifier ctx (WithSrcs sid _ g) = case g of
CLeaf (CIdentifier name) -> return $ WithSrc sid name
- _ -> throw $ ExpectedIdentifier ctx
+ _ -> throw sid $ ExpectedIdentifier ctx
aEffects :: WithSrcs ([GroupW], Maybe GroupW) -> SyntaxM (UEffectRow VoidS)
aEffects (WithSrcs _ _ (effs, optEffTail)) = do
@@ -364,7 +364,7 @@ aEffects (WithSrcs _ _ (effs, optEffTail)) = do
return $ UEffectRow (S.fromList lhs) rhs
effect :: GroupW -> SyntaxM (UEffect VoidS)
-effect (WithSrcs _ _ grp) = case grp of
+effect (WithSrcs grpSid _ grp) = case grp of
CParens [g] -> effect g
CJuxtapose True (Identifier "Read" ) (WithSrcs sid _ (CLeaf (CIdentifier h))) ->
return $ URWSEffect Reader $ fromSourceNameW (WithSrc sid h)
@@ -374,18 +374,18 @@ effect (WithSrcs _ _ grp) = case grp of
return $ URWSEffect State $ fromSourceNameW (WithSrc sid h)
CLeaf (CIdentifier "Except") -> return UExceptionEffect
CLeaf (CIdentifier "IO" ) -> return UIOEffect
- _ -> throw UnexpectedEffectForm
+ _ -> throw grpSid UnexpectedEffectForm
aMethod :: CSDeclW -> SyntaxM (Maybe (UMethodDef VoidS))
aMethod (WithSrcs _ _ CPass) = return Nothing
-aMethod (WithSrcs src _ d) = Just . WithSrcE src <$> case d of
+aMethod (WithSrcs sid _ d) = Just . WithSrcE sid <$> case d of
CDefDecl def -> do
- (WithSrc sid name, lam) <- aDef def
- return $ UMethodDef (SourceName sid name) lam
- CLet (WithSrcs sid _ (CLeaf (CIdentifier name))) rhs -> do
+ (WithSrc nameSid name, lam) <- aDef def
+ return $ UMethodDef (SourceName nameSid name) lam
+ CLet (WithSrcs lhsSid _ (CLeaf (CIdentifier name))) rhs -> do
rhs' <- ULamExpr Empty ImplicitApp Nothing Nothing <$> block rhs
- return $ UMethodDef (fromSourceNameW (WithSrc sid name)) rhs'
- _ -> throw UnexpectedMethodDef
+ return $ UMethodDef (fromSourceNameW (WithSrc lhsSid name)) rhs'
+ _ -> throw sid UnexpectedMethodDef
asExpr :: UBlock VoidS -> UExpr VoidS
asExpr (WithSrcE src b) = case b of
@@ -400,9 +400,9 @@ block (IndentedBlock sid decls) = do
blockDecls :: [CSDeclW] -> SyntaxM (Nest UDecl VoidS VoidS, UExpr VoidS)
blockDecls [] = error "shouldn't have empty list of decls"
-blockDecls [WithSrcs _ _ d] = case d of
+blockDecls [WithSrcs sid _ d] = case d of
CExpr g -> (Empty,) <$> expr g
- _ -> throw BlockWithoutFinalExpr
+ _ -> throw sid BlockWithoutFinalExpr
blockDecls (WithSrcs sid _ (CBind b rhs):ds) = do
b' <- binderOptTy Explicit b
rhs' <- asExpr <$> block rhs
@@ -427,7 +427,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
-- Table constructors here. Other uses of square brackets
-- should be detected upstream, before calling expr.
CBrackets gs -> UTabCon <$> mapM expr gs
- CGivens _ -> throw UnexpectedGivenClause
+ CGivens _ -> throw sid UnexpectedGivenClause
CArrow lhs effs rhs -> do
case lhs of
WithSrcs _ _ (CParens gs) -> do
@@ -435,7 +435,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
effs' <- fromMaybeM effs UPure aEffects
resultTy <- expr rhs
return $ UPi $ UPiExpr bs ExplicitApp effs' resultTy
- _ -> throw ArgsShouldHaveParens
+ WithSrcs lhsSid _ _ -> throw lhsSid ArgsShouldHaveParens
CDo b -> UDo <$> block b
CJuxtapose hasSpace lhs rhs -> case hasSpace of
True -> extendAppRight <$> expr lhs <*> expr rhs
@@ -454,26 +454,26 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
Pipe -> extendAppLeft <$> expr lhs <*> expr rhs
Dot -> do
lhs' <- expr lhs
- WithSrcs src _ rhs' <- return rhs
+ WithSrcs rhsSid _ rhs' <- return rhs
name <- case rhs' of
CLeaf (CIdentifier name) -> return $ FieldName name
CLeaf (CNat i ) -> return $ FieldNum $ fromIntegral i
- _ -> throw BadField
- return $ UFieldAccess lhs' (WithSrc src name)
+ _ -> throw rhsSid BadField
+ return $ UFieldAccess lhs' (WithSrc rhsSid name)
DoubleColon -> UTypeAnn <$> (expr lhs) <*> expr rhs
EvalBinOp s -> evalOp s
DepAmpersand -> do
lhs' <- tyOptPat lhs
UDepPairTy . (UDepPairType ExplicitDepPair lhs') <$> expr rhs
DepComma -> UDepPair <$> (expr lhs) <*> expr rhs
- CSEqual -> throw BadEqualSign
- Colon -> throw BadColon
+ CSEqual -> throw opSid BadEqualSign
+ Colon -> throw opSid BadColon
ImplicitArrow -> case lhs of
WithSrcs _ _ (CParens gs) -> do
bs <- aPiBinders gs
resultTy <- expr rhs
return $ UPi $ UPiExpr bs ImplicitApp UPure resultTy
- _ -> throw ArgsShouldHaveParens
+ WithSrcs lhsSid _ _ -> throw lhsSid ArgsShouldHaveParens
FatArrow -> do
lhs' <- tyOptPat lhs
UTabPi . (UTabPiExpr lhs') <$> expr rhs
@@ -483,7 +483,7 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
lhs' <- expr lhs
rhs' <- expr rhs
return $ explicitApp f [lhs', rhs']
- CPrefix (WithSrc _ name) g -> do
+ CPrefix (WithSrc prefixSid name) g -> do
case name of
"+" -> (withoutSrc <$> expr g) <&> \case
UNatLit i -> UIntLit (fromIntegral i)
@@ -494,8 +494,8 @@ expr (WithSrcs sid _ grp) = WithSrcE sid <$> case grp of
WithSrcE _ (UNatLit i) -> UIntLit (-(fromIntegral i))
WithSrcE _ (UIntLit i) -> UIntLit (-i)
WithSrcE _ (UFloatLit i) -> UFloatLit (-i)
- e -> unaryApp (mkUVar sid "neg") e
- _ -> throw $ BadPrefix $ pprint name
+ e -> unaryApp (mkUVar prefixSid "neg") e
+ _ -> throw prefixSid $ BadPrefix $ pprint name
CLambda params body -> do
params' <- explicitBindersOptAnn $ WithSrcs sid [] $ map stripParens params
body' <- block body
diff --git a/src/lib/Err.hs b/src/lib/Err.hs
index 649525f3..8a7037d2 100644
--- a/src/lib/Err.hs
+++ b/src/lib/Err.hs
@@ -14,7 +14,7 @@ module Err (
catchIOExcept, liftExcept, liftExceptAlt,
ignoreExcept, getCurrentCallStack, printCurrentCallStack,
ExceptT (..), rootSrcId, SrcId (..), assertEq, throwInternal,
- InferenceArgDesc, InfVarDesc (..)) where
+ InferenceArgDesc, InfVarDesc (..), HasSrcId (..)) where
import Control.Exception hiding (throw)
import Control.Applicative
@@ -43,6 +43,9 @@ newtype SrcId = SrcId Int deriving (Show, Eq, Ord, Generic)
rootSrcId :: SrcId
rootSrcId = SrcId 0
+class HasSrcId a where
+ getSrcId :: a -> SrcId
+
-- === core errro type ===
data Err =
@@ -464,8 +467,8 @@ instance Fallible HardFailM where
-- === convenience layer ===
-throw :: (ToErr e, Fallible m) => e -> m a
-throw e = throwErr $ toErr e
+throw :: (ToErr e, Fallible m) => SrcId -> e -> m a
+throw _ e = throwErr $ toErr e
{-# INLINE throw #-}
getCurrentCallStack :: () -> Maybe [String]
diff --git a/src/lib/Export.hs b/src/lib/Export.hs
index 85459572..67e356f6 100644
--- a/src/lib/Export.hs
+++ b/src/lib/Export.hs
@@ -48,11 +48,11 @@ prepareFunctionForExport :: (Mut n, Topper m)
prepareFunctionForExport cc f = do
naryPi <- case getType f of
TyCon (Pi piTy) -> return piTy
- _ -> throw $ MiscMiscErr "Only first-order functions can be exported"
+ _ -> throw rootSrcId $ MiscMiscErr "Only first-order functions can be exported"
sig <- liftExportSigM $ corePiToExportSig cc naryPi
closedSig <- case hoistToTop sig of
HoistFailure _ ->
- throw $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
+ throw rootSrcId $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
HoistSuccess s -> return s
f' <- liftBuilder $ buildCoreLam naryPi \xs -> naryApp (sink f) (toAtom <$> xs)
fSimp <- simplifyTopFunction $ coreLamToTopLam f'
@@ -68,7 +68,7 @@ prepareSLamForExport cc f@(TopLam _ naryPi _) = do
sig <- liftExportSigM $ simpPiToExportSig cc naryPi
closedSig <- case hoistToTop sig of
HoistFailure _ ->
- throw $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
+ throw rootSrcId $ MiscMiscErr $ "Types of exported functions have to be closed terms. Got: " ++ pprint naryPi
HoistSuccess s -> return s
fImp <- compileTopLevelFun cc f
nativeFun <- toCFunction "userFunc" fImp >>= emitObjFile >>= loadObject
@@ -105,7 +105,7 @@ corePiToExportSig :: CallingConvention
corePiToExportSig cc (CorePiType _ expls tbs (EffTy effs resultTy)) = do
case effs of
Pure -> return ()
- _ -> throw $ MiscMiscErr "Only pure functions can be exported"
+ _ -> throw rootSrcId $ MiscMiscErr "Only pure functions can be exported"
goArgs cc Empty [] (zipAttrs expls tbs) resultTy
simpPiToExportSig :: CallingConvention
@@ -113,7 +113,7 @@ simpPiToExportSig :: CallingConvention
simpPiToExportSig cc (PiType bs (EffTy effs resultTy)) = do
case effs of
Pure -> return ()
- _ -> throw $ MiscMiscErr "Only pure functions can be exported"
+ _ -> throw rootSrcId $ MiscMiscErr "Only pure functions can be exported"
bs' <- return $ fmapNest (\b -> WithAttrB Explicit b) bs
goArgs cc Empty [] bs' resultTy
@@ -164,7 +164,7 @@ toExportType ty = case ty of
Nothing -> unsupported
Just ety -> return ety
_ -> unsupported
- where unsupported = throw $ MiscMiscErr $ "Unsupported type of argument in exported function: " ++ pprint ty
+ where unsupported = throw rootSrcId $ MiscMiscErr $ "Unsupported type of argument in exported function: " ++ pprint ty
{-# INLINE toExportType #-}
parseTabTy :: IRRep r => Type r i -> ExportSigM r i o (Maybe (ExportType o))
diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs
index 67227f3d..cc10b171 100644
--- a/src/lib/Inference.hs
+++ b/src/lib/Inference.hs
@@ -47,6 +47,9 @@ import Types.Top
import qualified Types.OpNames as P
import Util hiding (group)
+sidtodo :: SrcId
+sidtodo = rootSrcId
+
-- === Top-level interface ===
checkTopUType :: (Fallible1 m, TopLogger m, EnvReader m) => UType n -> m n (CType n)
@@ -193,6 +196,9 @@ type Zonkable e = (HasNamesE e, SubstE AtomSubstVal e)
liftSolverM :: SolverM i o a -> InfererM i o a
liftSolverM cont = fst <$> runDiffStateT1 emptySolverSubst cont
+solverFail :: SolverM i o a
+solverFail = empty
+
zonk :: Zonkable e => e n -> SolverM i n (e n)
zonk e = do
s <- getDiffState
@@ -279,7 +285,7 @@ withFreshUnificationVar desc k cont = do
ans <- toAtomVar v >>= cont
soln <- (M.lookup v <$> fromSolverSubst <$> getDiffState) >>= \case
Just soln -> return soln
- Nothing -> throw $ AmbiguousInferenceVar (pprint v) (pprint k) desc
+ Nothing -> throw sidtodo $ AmbiguousInferenceVar (pprint v) (pprint k) desc
return (ans, soln)
{-# INLINE withFreshUnificationVar #-}
@@ -322,11 +328,11 @@ withFreshDictVarNoEmits dictTy synthIt cont = diffStateT1 \s -> do
{-# INLINE withFreshDictVarNoEmits #-}
withDict
- :: (Zonkable e, Emits o) => Kind CoreIR o
+ :: (Zonkable e, Emits o) => SrcId -> CType o
-> (forall o'. (Emits o', DExt o o') => CAtom o' -> SolverM i o' (e o'))
-> SolverM i o (e o)
-withDict dictTy cont = withFreshDictVar dictTy
- (\dictTy' -> lift11 $ trySynthTerm dictTy' Full)
+withDict sid dictTy cont = withFreshDictVar dictTy
+ (\dictTy' -> lift11 $ trySynthTerm sid dictTy' Full)
cont
{-# INLINE withDict#-}
@@ -353,14 +359,14 @@ emitTypeInfo sid ty = do
withReducibleEmissions
:: (HasNamesE e, SubstE AtomSubstVal e, ToErr err)
- => err
+ => SrcId -> err
-> (forall o' . (Emits o', DExt o o') => InfererM i o' (e o'))
-> InfererM i o (e o)
-withReducibleEmissions msg cont = do
+withReducibleEmissions sid msg cont = do
withDecls <- buildScoped cont
reduceWithDecls withDecls >>= \case
Just t -> return t
- _ -> throw msg
+ _ -> throw sid msg
{-# INLINE withReducibleEmissions #-}
-- === actual inference pass ===
@@ -391,13 +397,13 @@ topDown :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CAtom o)
topDown ty uexpr = topDownPartial (typeAsPartialType ty) uexpr
topDownPartial :: Emits o => PartialType o -> UExpr i -> InfererM i o (CAtom o)
-topDownPartial partialTy exprWithSrc@(WithSrcE _ expr) =
+topDownPartial partialTy exprWithSrc@(WithSrcE sid expr) =
case partialTy of
PartialType partialPiTy -> case expr of
- ULam lam -> toAtom <$> Lam <$> checkULamPartial partialPiTy lam
+ ULam lam -> toAtom <$> Lam <$> checkULamPartial partialPiTy sid lam
_ -> toAtom <$> Lam <$> etaExpandPartialPi partialPiTy \resultTy explicitArgs -> do
expr' <- bottomUpExplicit exprWithSrc
- dropSubst $ checkOrInferApp expr' explicitArgs [] resultTy
+ dropSubst $ checkOrInferApp sid sid expr' explicitArgs [] resultTy
FullType ty -> topDownExplicit ty exprWithSrc
-- Creates a lambda for all args and returns (via CPA) the explicit args
@@ -418,26 +424,26 @@ etaExpandPartialPi (PartialPiType appExpl expls bs effs reqTy) cont = do
-- Doesn't introduce implicit pi binders or dependent pairs
topDownExplicit :: forall i o. Emits o => CType o -> UExpr i -> InfererM i o (CAtom o)
-topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
+topDownExplicit reqTy exprWithSrc@(WithSrcE sid expr) = case expr of
ULam lamExpr -> case reqTy of
- TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam lamExpr piTy
- _ -> throw $ UnexpectedTerm "lambda" (pprint reqTy)
- UFor dir uFor -> case reqTy of
+ TyCon (Pi piTy) -> toAtom <$> Lam <$> checkULam sid lamExpr piTy
+ _ -> throw sid $ UnexpectedTerm "lambda" (pprint reqTy)
+ UFor dir uFor@(UForExpr b _) -> case reqTy of
TyCon (TabPi tabPiTy) -> do
- lam@(UnaryLamExpr b' _) <- checkUForExpr uFor tabPiTy
- ixTy <- asIxType $ binderType b'
+ lam@(UnaryLamExpr b' _) <- checkUForExpr sid uFor tabPiTy
+ ixTy <- asIxType (getSrcId b) $ binderType b'
emitHof $ For dir ixTy lam
- _ -> throw $ UnexpectedTerm "`for` expression" (pprint reqTy)
+ _ -> throw sid $ UnexpectedTerm "`for` expression" (pprint reqTy)
UApp f posArgs namedArgs -> do
f' <- bottomUpExplicit f
- checkOrInferApp f' posArgs namedArgs (Check reqTy)
+ checkOrInferApp sid (getSrcId f) f' posArgs namedArgs (Check reqTy)
UDepPair lhs rhs -> case reqTy of
TyCon (DepPairTy ty@(DepPairType _ (_ :> lhsTy) _)) -> do
lhs' <- checkSigmaDependent lhs (FullType lhsTy)
rhsTy <- instantiate ty [lhs']
rhs' <- topDown rhsTy rhs
return $ toAtom $ DepPair lhs' rhs' ty
- _ -> throw $ UnexpectedTerm "dependent pair" (pprint reqTy)
+ _ -> throw sid $ UnexpectedTerm "dependent pair" (pprint reqTy)
UCase scrut alts -> do
scrut' <- bottomUp scrut
let scrutTy = getType scrut'
@@ -446,16 +452,16 @@ topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
UDo block -> withBlockDecls block \result -> topDownExplicit (sink reqTy) result
UTabCon xs -> do
case reqTy of
- TyCon (TabPi tabPiTy) -> checkTabCon tabPiTy xs
- _ -> throw $ UnexpectedTerm "table constructor" (pprint reqTy)
- UNatLit x -> fromNatLit x reqTy
- UIntLit x -> fromIntLit x reqTy
+ TyCon (TabPi tabPiTy) -> checkTabCon tabPiTy sid xs
+ _ -> throw sid $ UnexpectedTerm "table constructor" (pprint reqTy)
+ UNatLit x -> fromNatLit sid x reqTy
+ UIntLit x -> fromIntLit sid x reqTy
UPrim UTuple xs -> case reqTy of
TyKind -> toAtom . ProdType <$> mapM checkUType xs
TyCon (ProdType reqTys) -> do
- when (length reqTys /= length xs) $ throw $ TupleLengthMismatch (length reqTys) (length xs)
+ when (length reqTys /= length xs) $ throw sid $ TupleLengthMismatch (length reqTys) (length xs)
toAtom <$> ProdCon <$> forM (zip reqTys xs) \(reqTy', x) -> topDown reqTy' x
- _ -> throw $ UnexpectedTerm "tuple" (pprint reqTy)
+ _ -> throw sid $ UnexpectedTerm "tuple" (pprint reqTy)
UFieldAccess _ _ -> infer
UVar _ -> infer
UTypeAnn _ _ -> infer
@@ -466,15 +472,15 @@ topDownExplicit reqTy exprWithSrc@(WithSrcE _ expr) = case expr of
UPi _ -> infer
UTabPi _ -> infer
UDepPairTy _ -> infer
- UHole -> throw InferHoleErr
+ UHole -> throw sid InferHoleErr
where
infer :: InfererM i o (CAtom o)
infer = do
sigmaAtom <- maybeInterpretPunsAsTyCons (Check reqTy) =<< bottomUpExplicit exprWithSrc
- instantiateSigma (Check reqTy) sigmaAtom
+ instantiateSigma sid (Check reqTy) sigmaAtom
bottomUp :: Emits o => UExpr i -> InfererM i o (CAtom o)
-bottomUp expr = bottomUpExplicit expr >>= instantiateSigma Infer
+bottomUp expr = bottomUpExplicit expr >>= instantiateSigma (getSrcId expr) Infer
-- Doesn't instantiate implicit args
bottomUpExplicit :: Emits o => UExpr i -> InfererM i o (SigmaAtom o)
@@ -488,7 +494,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
UFieldAccess x (WithSrc _ field) -> do
x' <- bottomUp x
ty <- return $ getType x'
- fields <- getFieldDefs ty
+ fields <- getFieldDefs sid ty
case M.lookup field fields of
Just def -> case def of
FieldProj i -> SigmaAtom Nothing <$> projectField i x'
@@ -496,18 +502,18 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
method' <- toAtomVar method
resultTy <- partialAppType (getType method') (params ++ [x'])
return $ SigmaPartialApp resultTy (toAtom method') (params ++ [x'])
- Nothing -> throw $ CantFindField (pprint field) (pprint ty) (map pprint $ M.keys fields)
+ Nothing -> throw sid $ CantFindField (pprint field) (pprint ty) (map pprint $ M.keys fields)
ULam lamExpr -> SigmaAtom Nothing <$> toAtom <$> inferULam lamExpr
- UFor dir uFor -> do
+ UFor dir uFor@(UForExpr b _) -> do
lam@(UnaryLamExpr b' _) <- inferUForExpr uFor
- ixTy <- asIxType $ binderType b'
+ ixTy <- asIxType (getSrcId b) $ binderType b'
liftM (SigmaAtom Nothing) $ emitHof $ For dir ixTy lam
UApp f posArgs namedArgs -> do
f' <- bottomUpExplicit f
- SigmaAtom Nothing <$> checkOrInferApp f' posArgs namedArgs Infer
+ SigmaAtom Nothing <$> checkOrInferApp sid (getSrcId f) f' posArgs namedArgs Infer
UTabApp tab args -> do
tab' <- bottomUp tab
- SigmaAtom Nothing <$> inferTabApp tab' args
+ SigmaAtom Nothing <$> inferTabApp (getSrcId tab) tab' args
UPi (UPiExpr bs appExpl effs ty) -> do
-- TODO: check explicitness constraints
withUBinders bs \(ZipB expls bs') -> do
@@ -517,26 +523,26 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
UTabPi (UTabPiExpr b ty) -> do
Abs b' ty' <- withUBinder b \(WithAttrB _ b') ->
liftM (Abs b') $ checkUType ty
- d <- getIxDict $ binderType b'
+ d <- getIxDict (getSrcId b) $ binderType b'
let piTy = TabPiType d b' ty'
return $ SigmaAtom Nothing $ toAtom $ TabPi piTy
UDepPairTy (UDepPairType expl b rhs) -> do
withUBinder b \(WithAttrB _ b') -> do
rhs' <- checkUType rhs
return $ SigmaAtom Nothing $ toAtom $ DepPairTy $ DepPairType expl b' rhs'
- UDepPair _ _ -> throw InferDepPairErr
+ UDepPair _ _ -> throw sid InferDepPairErr
UCase scrut (alt:alts) -> do
scrut' <- bottomUp scrut
let scrutTy = getType scrut'
alt'@(IndexedAlt _ altAbs) <- checkCaseAlt Infer scrutTy alt
Abs b ty <- liftEnvReaderM $ refreshAbs altAbs \b body -> do
return $ Abs b (getType body)
- resultTy <- liftHoistExcept $ hoist b ty
+ resultTy <- liftHoistExcept sid $ hoist b ty
alts' <- mapM (checkCaseAlt (Check resultTy) scrutTy) alts
SigmaAtom Nothing <$> buildSortedCase scrut' (alt':alts') resultTy
- UCase _ [] -> throw InferEmptyCaseEff
+ UCase _ [] -> throw sid InferEmptyCaseEff
UDo block -> withBlockDecls block \result -> bottomUpExplicit result
- UTabCon xs -> liftM (SigmaAtom Nothing) $ inferTabCon xs
+ UTabCon xs -> liftM (SigmaAtom Nothing) $ inferTabCon sid xs
UTypeAnn val ty -> do
ty' <- checkUType ty
liftM (SigmaAtom Nothing) $ topDown ty' val
@@ -550,7 +556,7 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
UPrim UExplicitApply (f:xs) -> do
f' <- bottomUpExplicit f
xs' <- mapM bottomUp xs
- SigmaAtom Nothing <$> applySigmaAtom f' xs'
+ SigmaAtom Nothing <$> applySigmaAtom sid f' xs'
UPrim UProjNewtype [x] -> do
x' <- bottomUp x >>= unwrapNewtype
return $ SigmaAtom Nothing x'
@@ -562,56 +568,56 @@ bottomUpExplicit (WithSrcE sid expr) = case expr of
_ -> return $ toAtom v
x' -> return x'
liftM (SigmaAtom Nothing) $ matchPrimApp prim xs'
- UNatLit l -> liftM (SigmaAtom Nothing) $ fromNatLit l NatTy
- UIntLit l -> liftM (SigmaAtom Nothing) $ fromIntLit l (BaseTy $ Scalar Int32Type)
+ UNatLit l -> liftM (SigmaAtom Nothing) $ fromNatLit sid l NatTy
+ UIntLit l -> liftM (SigmaAtom Nothing) $ fromIntLit sid l (BaseTy $ Scalar Int32Type)
UFloatLit x -> return $ SigmaAtom Nothing $ Con $ Lit $ Float32Lit $ realToFrac x
- UHole -> throw InferHoleErr
+ UHole -> throw sid InferHoleErr
-expectEq :: (PrettyE e, AlphaEqE e) => e o -> e o -> InfererM i o ()
-expectEq reqTy actualTy = alphaEq reqTy actualTy >>= \case
+expectEq :: (PrettyE e, AlphaEqE e) => SrcId -> e o -> e o -> InfererM i o ()
+expectEq sid reqTy actualTy = alphaEq reqTy actualTy >>= \case
True -> return ()
- False -> throw $ TypeMismatch (pprint reqTy) (pprint actualTy)
+ False -> throw sid $ TypeMismatch (pprint reqTy) (pprint actualTy)
{-# INLINE expectEq #-}
-fromIntLit :: Emits o => Int -> CType o -> InfererM i o (CAtom o)
-fromIntLit x ty = do
+fromIntLit :: Emits o => SrcId -> Int -> CType o -> InfererM i o (CAtom o)
+fromIntLit sid x ty = do
let litVal = Con $ Lit $ Int64Lit $ fromIntegral x
- applyFromLiteralMethod ty "from_integer" litVal
+ applyFromLiteralMethod sid ty "from_integer" litVal
-fromNatLit :: Emits o => Word64 -> CType o -> InfererM i o (CAtom o)
-fromNatLit x ty = do
+fromNatLit :: Emits o => SrcId -> Word64 -> CType o -> InfererM i o (CAtom o)
+fromNatLit sid x ty = do
let litVal = Con $ Lit $ Word64Lit $ fromIntegral x
- applyFromLiteralMethod ty "from_unsigned_integer" litVal
-
-matchReq :: Ext o o' => RequiredTy o -> CAtom o' -> InfererM i o' (CAtom o')
-matchReq (Check reqTy) x = do
- reqTy' <- sinkM reqTy
- return x <* expectEq reqTy' (getType x)
-matchReq Infer x = return x
-{-# INLINE matchReq #-}
+ applyFromLiteralMethod sid ty "from_unsigned_integer" litVal
-instantiateSigma :: Emits o => RequiredTy o -> SigmaAtom o -> InfererM i o (CAtom o)
-instantiateSigma reqTy sigmaAtom = case sigmaAtom of
+instantiateSigma :: Emits o => SrcId -> RequiredTy o -> SigmaAtom o -> InfererM i o (CAtom o)
+instantiateSigma sid reqTy sigmaAtom = case sigmaAtom of
SigmaUVar _ _ _ -> case getType sigmaAtom of
TyCon (Pi (CorePiType ImplicitApp expls bs (EffTy _ resultTy))) -> do
bsConstrained <- buildConstraints (Abs bs resultTy) \_ resultTy' -> do
case reqTy of
Infer -> return []
- Check reqTy' -> return [TypeConstraint (sink reqTy') resultTy']
+ Check reqTy' -> return [TypeConstraint sidtodo (sink reqTy') resultTy']
args <- inferMixedArgs @UExpr fDesc expls bsConstrained ([], [])
- applySigmaAtom sigmaAtom args
+ applySigmaAtom sidtodo sigmaAtom args
_ -> fallback
_ -> fallback
where
- fallback = forceSigmaAtom sigmaAtom >>= matchReq reqTy
+ fallback = forceSigmaAtom sigmaAtom >>= matchReq sid reqTy
fDesc = getSourceName sigmaAtom
+matchReq :: Ext o o' => SrcId -> RequiredTy o -> CAtom o' -> InfererM i o' (CAtom o')
+matchReq sid (Check reqTy) x = do
+ reqTy' <- sinkM reqTy
+ return x <* expectEq sid reqTy' (getType x)
+matchReq _ Infer x = return x
+{-# INLINE matchReq #-}
+
forceSigmaAtom :: Emits o => SigmaAtom o -> InfererM i o (CAtom o)
forceSigmaAtom sigmaAtom = case sigmaAtom of
SigmaAtom _ x -> return x
SigmaUVar _ _ v -> case v of
UAtomVar v' -> inlineTypeAliases v'
- _ -> applySigmaAtom sigmaAtom []
+ _ -> applySigmaAtom sidtodo sigmaAtom []
SigmaPartialApp _ _ _ -> error "not implemented" -- better error message?
withBlockDecls
@@ -649,14 +655,14 @@ considerInlineAnn PlainLet (TyCon (Pi (CorePiType _ _ _ (EffTy Pure TyKind)))) =
considerInlineAnn ann _ = ann
applyFromLiteralMethod
- :: Emits n => CType n -> SourceName -> CAtom n -> InfererM i n (CAtom n)
-applyFromLiteralMethod resultTy methodName litVal =
+ :: Emits n => SrcId -> CType n -> SourceName -> CAtom n -> InfererM i n (CAtom n)
+applyFromLiteralMethod sid resultTy methodName litVal =
lookupSourceMap methodName >>= \case
Nothing -> error $ "prelude function not found: " ++ pprint methodName
Just ~(UMethodVar methodName') -> do
MethodBinding className _ <- lookupEnv methodName'
dictTy <- toType <$> dictType className [toAtom resultTy]
- Just d <- toMaybeDict <$> trySynthTerm dictTy Full
+ Just d <- toMaybeDict <$> trySynthTerm sid dictTy Full
emit =<< mkApplyMethod d 0 [litVal]
-- atom that requires instantiation to become a rho type
@@ -687,8 +693,8 @@ data FieldDef (n::S) =
| FieldDotMethod (CAtomName n) (TyConParams n)
deriving (Show, Generic)
-getFieldDefs :: CType n -> InfererM i n (M.Map FieldName' (FieldDef n))
-getFieldDefs ty = case ty of
+getFieldDefs :: SrcId -> CType n -> InfererM i n (M.Map FieldName' (FieldDef n))
+getFieldDefs sid ty = case ty of
StuckTy _ _ -> noFields
TyCon con -> case con of
NewtypeTyCon (UserADTType _ tyName params) -> do
@@ -704,7 +710,7 @@ getFieldDefs ty = case ty of
RefType _ valTy -> case valTy of
RefTy _ _ -> noFields
_ -> do
- valFields <- getFieldDefs valTy
+ valFields <- getFieldDefs sid valTy
return $ M.filter isProj valFields
where isProj = \case
FieldProj _ -> True
@@ -712,7 +718,7 @@ getFieldDefs ty = case ty of
ProdType ts -> return $ M.fromList $ enumerate ts <&> \(i, _) -> (FieldNum i, FieldProj i)
TabPi _ -> noFields
_ -> noFields
- where noFields = throw $ NoFields $ pprint ty
+ where noFields = throw sid $ NoFields $ pprint ty
projectField :: Emits o => Int -> CAtom o -> InfererM i o (CAtom o)
projectField i x = case getType x of
@@ -751,40 +757,40 @@ checkCAtom :: CAtom i -> PartialType o -> InfererM i o (CAtom o)
checkCAtom arg argTy = do
arg' <- renameM arg
case argTy of
- FullType argTy' -> expectEq argTy' (getType arg')
+ FullType argTy' -> expectEq sidtodo argTy' (getType arg')
PartialType _ -> return () -- TODO?
return arg'
checkOrInferApp
:: forall i o arg . (Emits o, ExplicitArg arg)
- => SigmaAtom o -> [arg i] -> [(SourceName, arg i)]
+ => SrcId -> SrcId -> SigmaAtom o -> [arg i] -> [(SourceName, arg i)]
-> RequiredTy o -> InfererM i o (CAtom o)
-checkOrInferApp f' posArgs namedArgs reqTy = do
+checkOrInferApp appSrcId funSrcId f' posArgs namedArgs reqTy = do
f <- maybeInterpretPunsAsTyCons reqTy f'
case getType f of
TyCon (Pi piTy@(CorePiType appExpl expls _ _)) -> case appExpl of
ExplicitApp -> do
- checkExplicitArity expls posArgs
- bsConstrained <- buildAppConstraints reqTy piTy
+ checkExplicitArity appSrcId expls posArgs
+ bsConstrained <- buildAppConstraints appSrcId reqTy piTy
args <- inferMixedArgs fDesc expls bsConstrained (posArgs, namedArgs)
- applySigmaAtom f args
+ applySigmaAtom appSrcId f args
ImplicitApp -> error "should already have handled this case"
- ty -> throw $ EliminationErr "function type" (pprint ty)
+ ty -> throw funSrcId $ EliminationErr "function type" (pprint ty)
where
fDesc :: SourceName
fDesc = getSourceName f'
-buildAppConstraints :: RequiredTy n -> CorePiType n -> InfererM i n (ConstrainedBinders n)
-buildAppConstraints reqTy (CorePiType _ _ bs effTy) = do
+buildAppConstraints :: SrcId -> RequiredTy n -> CorePiType n -> InfererM i n (ConstrainedBinders n)
+buildAppConstraints appSrcId reqTy (CorePiType _ _ bs effTy) = do
effsAllowed <- infEffects <$> getInfState
buildConstraints (Abs bs effTy) \_ (EffTy effs resultTy) -> do
resultTyConstraints <- return case reqTy of
Infer -> []
- Check reqTy' -> [TypeConstraint (sink reqTy') resultTy]
+ Check reqTy' -> [TypeConstraint appSrcId (sink reqTy') resultTy]
EffectRow _ t <- return effs
effConstraints <- case t of
NoTail -> return []
- EffectRowTail _ -> return [EffectConstraint (sink effsAllowed) effs]
+ EffectRowTail _ -> return [EffectConstraint appSrcId (sink effsAllowed) effs]
return $ resultTyConstraints ++ effConstraints
maybeInterpretPunsAsTyCons :: RequiredTy n -> SigmaAtom n -> InfererM i n (SigmaAtom n)
@@ -802,12 +808,12 @@ inlineTypeAliases v = do
LetBound (DeclBinding InlineLet (Atom e)) -> return e
_ -> toAtom <$> toAtomVar v
-applySigmaAtom :: Emits o => SigmaAtom o -> [CAtom o] -> InfererM i o (CAtom o)
-applySigmaAtom (SigmaAtom _ f) args = emitWithEffects =<< mkApp f args
-applySigmaAtom (SigmaUVar _ _ f) args = case f of
+applySigmaAtom :: Emits o => SrcId -> SigmaAtom o -> [CAtom o] -> InfererM i o (CAtom o)
+applySigmaAtom appSrcId (SigmaAtom _ f) args = emitWithEffects appSrcId =<< mkApp f args
+applySigmaAtom appSrcId (SigmaUVar _ _ f) args = case f of
UAtomVar f' -> do
f'' <- inlineTypeAliases f'
- emitWithEffects =<< mkApp f'' args
+ emitWithEffects appSrcId =<< mkApp f'' args
UTyConVar f' -> do
TyConDef sn roleExpls _ _ <- lookupTyCon f'
let expls = snd <$> roleExpls
@@ -836,9 +842,9 @@ applySigmaAtom (SigmaUVar _ _ f) args = case f of
let numParams = nestLength paramBs
-- params aren't needed because they're already implied by the dict argument
let (dictArg:args') = drop numParams args
- emitWithEffects =<< mkApplyMethod (fromJust $ toMaybeDict dictArg) methodIdx args'
-applySigmaAtom (SigmaPartialApp _ f prevArgs) args =
- emitWithEffects =<< mkApp f (prevArgs ++ args)
+ emitWithEffects appSrcId =<< mkApplyMethod (fromJust $ toMaybeDict dictArg) methodIdx args'
+applySigmaAtom appSrcId (SigmaPartialApp _ f prevArgs) args =
+ emitWithEffects appSrcId =<< mkApp f (prevArgs ++ args)
splitParamPrefix :: EnvReader m => TyConName n -> [CAtom n] -> m n (TyConParams n, [CAtom n])
splitParamPrefix tc args = do
@@ -878,22 +884,22 @@ applyDataCon tc conIx topArgs = do
where h:t = args
_ -> error $ "Unexpected data con representation type: " ++ pprint rty
-emitWithEffects :: Emits o => CExpr o -> InfererM i o (CAtom o)
-emitWithEffects expr = do
- addEffects $ getEffects expr
+emitWithEffects :: Emits o => SrcId -> CExpr o -> InfererM i o (CAtom o)
+emitWithEffects sid expr = do
+ addEffects sid $ getEffects expr
emit expr
-checkExplicitArity :: [Explicitness] -> [a] -> InfererM i o ()
-checkExplicitArity expls args = do
+checkExplicitArity :: SrcId -> [Explicitness] -> [a] -> InfererM i o ()
+checkExplicitArity sid expls args = do
let arity = length [() | Explicit <- expls]
let numArgs = length args
- when (numArgs /= arity) $ throw $ ArityErr arity numArgs
+ when (numArgs /= arity) $ throw sid $ ArityErr arity numArgs
type MixedArgs arg = ([arg], [(SourceName, arg)]) -- positional args, named args
data Constraint (n::S) =
- TypeConstraint (CType n) (CType n)
+ TypeConstraint SrcId (CType n) (CType n)
-- permitted effects (no inference vars), proposed effects
- | EffectConstraint (EffectRow CoreIR n) (EffectRow CoreIR n)
+ | EffectConstraint SrcId (EffectRow CoreIR n) (EffectRow CoreIR n)
type Constraints = ListE Constraint
type ConstrainedBinders n = ([IsDependent], Abs (Nest CBinder) Constraints n)
@@ -944,8 +950,8 @@ inferMixedArgs fSourceName explsTop (dependenceTop, bsAbs) argsTop@(_, namedArgs
eagerlyApplyConstraints bs (ListE cs) = ListE <$> forMFilter cs \c -> do
case hoist bs c of
HoistSuccess c' -> case c' of
- TypeConstraint _ _ -> applyConstraint c' >> return Nothing
- EffectConstraint _ (EffectRow specificEffs _) ->
+ TypeConstraint _ _ _ -> applyConstraint c' >> return Nothing
+ EffectConstraint _ _ (EffectRow specificEffs _) ->
hasInferenceVars specificEffs >>= \case
False -> applyConstraint c' >> return Nothing
-- we delay applying the constraint in this case because we might
@@ -980,7 +986,7 @@ inferMixedArgs fSourceName explsTop (dependenceTop, bsAbs) argsTop@(_, namedArgs
withDistinct $ cont arg' args
Nothing -> case infMech of
Unify -> withFreshUnificationVar (ImplicitArgInfVar desc) argTy \v -> cont (toAtom v) args
- Synth _ -> withDict argTy \d -> cont d args
+ Synth _ -> withDict sidtodo argTy \d -> cont d args
checkOrInferExplicitArg :: Emits oo => Bool -> arg i -> CType oo -> SolverM i oo (CAtom oo)
checkOrInferExplicitArg isDependent arg argTy = do
@@ -989,7 +995,7 @@ inferMixedArgs fSourceName explsTop (dependenceTop, bsAbs) argsTop@(_, namedArgs
True -> checkExplicitDependentArg arg partialTy
False -> checkExplicitNonDependentArg arg partialTy
Nothing -> inferExplicitArg arg
- constrainEq argTy (getType arg')
+ constrainEq sidtodo argTy (getType arg')
return arg'
lookupNamedArg :: MixedArgs x -> Maybe SourceName -> Maybe x
@@ -1016,10 +1022,11 @@ checkNamedArgValidity expls offeredNames = do
Inferred v _ -> v
let acceptedNames = catMaybes $ map explToMaybeName expls
let duplicates = repeated offeredNames
- when (not $ null duplicates) $ throw $ RepeatedOptionalArgs $ map pprint duplicates
+ -- here and below we should be able to get a per-name src id
+ when (not $ null duplicates) $ throw sidtodo $ RepeatedOptionalArgs $ map pprint duplicates
let unrecognizedNames = filter (not . (`elem` acceptedNames)) offeredNames
when (not $ null unrecognizedNames) do
- throw $ UnrecognizedOptionalArgs (map pprint unrecognizedNames) (map pprint acceptedNames)
+ throw sidtodo $ UnrecognizedOptionalArgs (map pprint unrecognizedNames) (map pprint acceptedNames)
inferPrimArg :: Emits o => UExpr i -> InfererM i o (CAtom o)
inferPrimArg x = do
@@ -1101,15 +1108,15 @@ pattern ExplicitCoreLam bs body <- Con (Lam (CoreLamExpr _ (LamExpr bs body)))
-- === n-ary applications ===
-inferTabApp :: Emits o => CAtom o -> [UExpr i] -> InfererM i o (CAtom o)
-inferTabApp tab args = do
+inferTabApp :: Emits o => SrcId -> CAtom o -> [UExpr i] -> InfererM i o (CAtom o)
+inferTabApp tabSrcId tab args = do
tabTy <- return $ getType tab
- args' <- inferNaryTabAppArgs tabTy args
+ args' <- inferNaryTabAppArgs tabSrcId tabTy args
naryTabApp tab args'
-inferNaryTabAppArgs :: Emits o => CType o -> [UExpr i] -> InfererM i o [CAtom o]
-inferNaryTabAppArgs _ [] = return []
-inferNaryTabAppArgs tabTy (arg:rest) = case tabTy of
+inferNaryTabAppArgs :: Emits o => SrcId -> CType o -> [UExpr i] -> InfererM i o [CAtom o]
+inferNaryTabAppArgs _ _ [] = return []
+inferNaryTabAppArgs tabSrcId tabTy (arg:rest) = case tabTy of
TyCon (TabPi (TabPiType _ b resultTy)) -> do
let ixTy = binderType b
let isDependent = binderName b `isFreeIn` resultTy
@@ -1117,12 +1124,12 @@ inferNaryTabAppArgs tabTy (arg:rest) = case tabTy of
then checkSigmaDependent arg (FullType ixTy)
else topDown ixTy arg
resultTy' <- applySubst (b @> SubstVal arg') resultTy
- rest' <- inferNaryTabAppArgs resultTy' rest
+ rest' <- inferNaryTabAppArgs tabSrcId resultTy' rest
return $ arg':rest'
- _ -> throw $ EliminationErr "table type" (pprint tabTy)
+ _ -> throw tabSrcId $ EliminationErr "table type" (pprint tabTy)
checkSigmaDependent :: UExpr i -> PartialType o -> InfererM i o (CAtom o)
-checkSigmaDependent e ty = withReducibleEmissions CantReduceDependentArg $
+checkSigmaDependent e ty = withReducibleEmissions (getSrcId e) CantReduceDependentArg $
topDownPartial (sink ty) e
-- === sorting case alternatives ===
@@ -1271,10 +1278,11 @@ inferClassDef className methodNames paramBs methodTys = do
checkUType m >>= \case
TyCon (Pi t) -> return t
t -> return $ CorePiType ImplicitApp [] Empty (EffTy Pure t)
- PairB paramBs'' superclassBs <- partitionBinders (zipAttrs roleExpls paramBs') $
+ PairB paramBs'' superclassBs <- partitionBinders rootSrcId (zipAttrs roleExpls paramBs') $
\b@(WithAttrB (_, expl) b') -> case expl of
Explicit -> return $ LeftB b
- Inferred _ Unify -> throw InterfacesNoImplicitParams
+ -- TODO: Add a proper SrcId here. We'll need to plumb it through from the original UBinders
+ Inferred _ Unify -> throw rootSrcId InterfacesNoImplicitParams
Inferred _ (Synth _) -> return $ RightB b'
let (roleExpls', paramBs''') = unzipAttrs paramBs''
builtinName <- case className of
@@ -1287,7 +1295,7 @@ inferClassDef className methodNames paramBs methodTys = do
withUBinder :: UAnnBinder i i' -> InfererCPSB2 (WithExpl CBinder) i i' o a
withUBinder (UAnnBinder expl b ann cs) cont = do
- ty <- inferAnn ann cs
+ ty <- inferAnn (getSrcId b) ann cs
withFreshBinderInf (getNameHint b) expl ty \b' ->
extendSubst (b@>binderName b') $ cont (WithAttrB expl b')
@@ -1307,7 +1315,7 @@ inferUBinders Empty cont = withDistinct $ Abs Empty <$> cont []
inferUBinders (Nest (UAnnBinder expl b ann cs) bs) cont = do
-- TODO: factor out the common part of each case (requires an annotated
-- `where` clause because of the rank-2 type)
- ty <- inferAnn ann cs
+ ty <- inferAnn (getSrcId b) ann cs
withFreshBinderInf (getNameHint b) expl ty \b' -> do
extendSubst (b@>binderName b') do
Abs bs' e <- inferUBinders bs \vs -> cont (sink (binderName b') : vs)
@@ -1336,32 +1344,32 @@ withRoleUBinders bs cont = do
False -> return DataParam
{-# INLINE inferRole #-}
-inferAnn :: UAnn i -> [UConstraint i] -> InfererM i o (CType o)
-inferAnn ann cs = case ann of
+inferAnn :: SrcId -> UAnn i -> [UConstraint i] -> InfererM i o (CType o)
+inferAnn binderSrcId ann cs = case ann of
UAnn ty -> checkUType ty
UNoAnn -> case cs of
- WithSrcE _ (UVar ~(InternalName _ _ v)):_ -> do
+ WithSrcE sid (UVar ~(InternalName _ _ v)):_ -> do
renameM v >>= getUVarType >>= \case
TyCon (Pi (CorePiType ExplicitApp [Explicit] (UnaryNest (_:>ty)) _)) -> return ty
- ty -> throw $ NotAUnaryConstraint $ pprint ty
- _ -> throw AnnotationRequired
+ ty -> throw sid $ NotAUnaryConstraint $ pprint ty
+ _ -> throw binderSrcId AnnotationRequired
-checkULamPartial :: PartialPiType o -> ULamExpr i -> InfererM i o (CoreLamExpr o)
-checkULamPartial partialPiTy lamExpr = do
+checkULamPartial :: PartialPiType o -> SrcId -> ULamExpr i -> InfererM i o (CoreLamExpr o)
+checkULamPartial partialPiTy sid lamExpr = do
PartialPiType piAppExpl expls piBs piEffs piReqTy <- return partialPiTy
ULamExpr lamBs lamAppExpl lamEffs lamResultTy body <- return lamExpr
- checkExplicitArity expls (nestToList (const ()) lamBs)
- when (piAppExpl /= lamAppExpl) $ throw $ WrongArrowErr (pprint piAppExpl) (pprint lamAppExpl)
+ checkExplicitArity sid expls (nestToList (const ()) lamBs)
+ when (piAppExpl /= lamAppExpl) $ throw sid $ WrongArrowErr (pprint piAppExpl) (pprint lamAppExpl)
checkLamBinders expls piBs lamBs \lamBs' -> do
PairE piEffs' piReqTy' <- applyRename (piBs @@> (atomVarName <$> bindersVars lamBs')) (PairE piEffs piReqTy)
resultTy <- case (lamResultTy, piReqTy') of
(Nothing, Infer ) -> return Infer
(Just t , Infer ) -> Check <$> checkUType t
(Nothing, Check t) -> Check <$> return t
- (Just t , Check t') -> checkUType t >>= expectEq t' >> return (Check t')
+ (Just t , Check t') -> checkUType t >>= expectEq (getSrcId t) t' >> return (Check t')
forM_ lamEffs \lamEffs' -> do
lamEffs'' <- checkUEffRow lamEffs'
- expectEq (Eff piEffs') (Eff lamEffs'')
+ expectEq sid (Eff piEffs') (Eff lamEffs'') -- TODO: add source annotations to lambda effects too
body' <- withAllowedEffects piEffs' do
buildBlock $ withBlockDecls body \result -> checkOrInfer (sink resultTy) result
resultTy' <- case resultTy of
@@ -1383,7 +1391,7 @@ checkULamPartial partialPiTy lamExpr = do
Explicit -> case lamBs of
Nest (UAnnBinder _ lamB lamAnn _) lamBsRest -> do
case lamAnn of
- UAnn lamAnn' -> checkUType lamAnn' >>= expectEq piAnn
+ UAnn lamAnn' -> checkUType lamAnn' >>= expectEq (getSrcId lamAnn') piAnn
UNoAnn -> return ()
withFreshBinderInf (getNameHint lamB) Explicit piAnn \b -> do
Abs piBs' UnitE <- applyRename (piB@>binderName b) (EmptyAbs piBs)
@@ -1398,13 +1406,13 @@ inferUForExpr (UForExpr b body) = do
body' <- buildBlock $ withBlockDecls body \result -> bottomUp result
return $ LamExpr (UnaryNest b') body'
-checkUForExpr :: Emits o => UForExpr i -> TabPiType CoreIR o -> InfererM i o (LamExpr CoreIR o)
-checkUForExpr (UForExpr bFor body) (TabPiType _ bPi resultTy) = do
+checkUForExpr :: Emits o => SrcId -> UForExpr i -> TabPiType CoreIR o -> InfererM i o (LamExpr CoreIR o)
+checkUForExpr sid (UForExpr bFor body) (TabPiType _ bPi resultTy) = do
let uLamExpr = ULamExpr (UnaryNest bFor) ExplicitApp Nothing Nothing body
effsAllowed <- infEffects <$> getInfState
partialPi <- liftEnvReaderM $ refreshAbs (Abs bPi resultTy) \bPi' resultTy' -> do
return $ PartialPiType ExplicitApp [Explicit] (UnaryNest bPi') (sink effsAllowed) (Check resultTy')
- CoreLamExpr _ lamExpr <- checkULamPartial partialPi uLamExpr
+ CoreLamExpr _ lamExpr <- checkULamPartial partialPi sid uLamExpr
return lamExpr
inferULam :: ULamExpr i -> InfererM i o (CoreLamExpr o)
@@ -1421,8 +1429,8 @@ inferULam (ULamExpr bs appExpl effs resultTy body) = do
return $ PairE effTy body'
return $ CoreLamExpr (CorePiType appExpl expls bs' effTy) (LamExpr bs' body')
-checkULam :: ULamExpr i -> CorePiType o -> InfererM i o (CoreLamExpr o)
-checkULam ulam piTy = checkULamPartial (piAsPartialPi piTy) ulam
+checkULam :: SrcId -> ULamExpr i -> CorePiType o -> InfererM i o (CoreLamExpr o)
+checkULam sid ulam piTy = checkULamPartial (piAsPartialPi piTy) sid ulam
piAsPartialPi :: CorePiType n -> PartialPiType n
piAsPartialPi (CorePiType appExpl expls bs (EffTy effs ty)) =
@@ -1451,48 +1459,52 @@ checkInstanceBody
:: ClassName o -> [CAtom o]
-> [UMethodDef i] -> InfererM i o (InstanceBody o)
checkInstanceBody className params methods = do
+ -- instances are top-level so it's ok to have imprecise root srcIds here
+ let sid = rootSrcId
ClassDef _ _ methodNames _ _ paramBs scBs methodTys <- lookupClassDef className
Abs scBs' methodTys' <- applySubst (paramBs @@> (SubstVal <$> params)) $ Abs scBs $ ListE methodTys
superclassTys <- superclassDictTys scBs'
- superclassDicts <- mapM (flip trySynthTerm Full) superclassTys
+ superclassDicts <- mapM (flip (trySynthTerm sid) Full) superclassTys
ListE methodTys'' <- applySubst (scBs'@@>(SubstVal<$>superclassDicts)) methodTys'
methodsChecked <- mapM (checkMethodDef className methodTys'') methods
let (idxs, methods') = unzip $ sortOn fst $ methodsChecked
- forM_ (repeated idxs) \i -> throw $ DuplicateMethod $ pprint (methodNames!!i)
- forM_ ([0..(length methodTys''-1)] `listDiff` idxs) \i -> throw $ MissingMethod $ pprint (methodNames!!i)
+ forM_ (repeated idxs) \i ->
+ throw sid $ DuplicateMethod $ pprint (methodNames!!i)
+ forM_ ([0..(length methodTys''-1)] `listDiff` idxs) \i ->
+ throw sid $ MissingMethod $ pprint (methodNames!!i)
return $ InstanceBody superclassDicts methods'
superclassDictTys :: Nest CBinder o o' -> InfererM i o [CType o]
superclassDictTys Empty = return []
superclassDictTys (Nest b bs) = do
- Abs bs' UnitE <- liftHoistExcept $ hoist b $ Abs bs UnitE
+ Abs bs' UnitE <- liftHoistExcept sidtodo $ hoist b $ Abs bs UnitE
(binderType b:) <$> superclassDictTys bs'
checkMethodDef :: ClassName o -> [CorePiType o] -> UMethodDef i -> InfererM i o (Int, CAtom o)
-checkMethodDef className methodTys (WithSrcE _ m) = do
+checkMethodDef className methodTys (WithSrcE sid m) = do
UMethodDef ~(InternalName _ sourceName v) rhs <- return m
MethodBinding className' i <- renameM v >>= lookupEnv
when (className /= className') do
ClassBinding classDef <- lookupEnv className
- throw $ NotAMethod (pprint sourceName) (pprint $ getSourceName classDef)
- (i,) <$> toAtom <$> Lam <$> checkULam rhs (methodTys !! i)
+ throw sid $ NotAMethod (pprint sourceName) (pprint $ getSourceName classDef)
+ (i,) <$> toAtom <$> Lam <$> checkULam sid rhs (methodTys !! i)
checkUEffRow :: UEffectRow i -> InfererM i o (EffectRow CoreIR o)
checkUEffRow (UEffectRow effs t) = do
effs' <- liftM eSetFromList $ mapM checkUEff $ toList effs
t' <- case t of
Nothing -> return NoTail
- Just (SourceOrInternalName ~(InternalName _ _ v)) -> do
+ Just (SourceOrInternalName ~(InternalName sid _ v)) -> do
v' <- toAtomVar =<< renameM v
- expectEq EffKind (getType v')
+ expectEq sid EffKind (getType v')
return $ EffectRowTail v'
return $ EffectRow effs' t'
checkUEff :: UEffect i -> InfererM i o (Effect CoreIR o)
checkUEff eff = case eff of
- URWSEffect rws (SourceOrInternalName ~(InternalName _ _ region)) -> do
+ URWSEffect rws (SourceOrInternalName ~(InternalName sid _ region)) -> do
region' <- renameM region >>= toAtomVar
- expectEq (TyCon HeapType) (getType region')
+ expectEq sid (TyCon HeapType) (getType region')
return $ RWSEffect rws (toAtom region')
UExceptionEffect -> return ExceptionEffect
UIOEffect -> return IOEffect
@@ -1507,31 +1519,31 @@ checkCaseAlt reqTy scrutineeTy (UAlt pat body) = do
return $ IndexedAlt idx alt
getCaseAltIndex :: UPat i i' -> InfererM i o CaseAltIndex
-getCaseAltIndex (WithSrcB _ pat) = case pat of
+getCaseAltIndex (WithSrcB sid pat) = case pat of
UPatCon ~(InternalName _ _ conName) _ -> do
(_, con) <- renameM conName >>= lookupDataCon
return con
- _ -> throw IllFormedCasePattern
+ _ -> throw sid IllFormedCasePattern
checkCasePat
:: Emits o
=> UPat i i' -> CType o
-> (forall o'. (Emits o', Ext o o') => InfererM i' o' (CAtom o'))
-> InfererM i o (Alt CoreIR o)
-checkCasePat (WithSrcB _ pat) scrutineeTy cont = case pat of
+checkCasePat (WithSrcB sid pat) scrutineeTy cont = case pat of
UPatCon ~(InternalName _ _ conName) ps -> do
(dataDefName, con) <- renameM conName >>= lookupDataCon
tyConDef <- lookupTyCon dataDefName
params <- inferParams scrutineeTy dataDefName
ADTCons cons <- instantiateTyConDef tyConDef params
DataConDef _ _ repTy idxs <- return $ cons !! con
- when (length idxs /= nestLength ps) $ throw $ PatternArityErr (length idxs) (nestLength ps)
+ when (length idxs /= nestLength ps) $ throw sid $ PatternArityErr (length idxs) (nestLength ps)
withFreshBinderInf noHint Explicit repTy \b -> Abs b <$> do
buildBlock do
args <- forM idxs \projs -> do
emitToVar =<< applyProjectionsReduced (init projs) (sink $ toAtom $ binderVar b)
bindLetPats ps args $ cont
- _ -> throw IllFormedCasePattern
+ _ -> throw sid IllFormedCasePattern
inferParams :: Emits o => CType o -> TyConName o -> InfererM i o (TyConParams o)
inferParams ty dataDefName = do
@@ -1542,7 +1554,7 @@ inferParams ty dataDefName = do
expl -> expl
paramBsAbs <- buildConstraints (Abs paramBs UnitE) \params _ -> do
let ty' = toType $ UserADTType sourceName (sink dataDefName) $ TyConParams paramExpls params
- return [TypeConstraint (sink ty) ty']
+ return [TypeConstraint sidtodo (sink ty) ty']
args <- inferMixedArgs sourceName inferenceExpls paramBsAbs emptyMixedArgs
return $ TyConParams paramExpls args
@@ -1560,19 +1572,19 @@ bindLetPat
=> UPat i i' -> CAtomVar o
-> (forall o'. (Emits o', DExt o o') => InfererM i' o' (e o'))
-> InfererM i o (e o)
-bindLetPat (WithSrcB _ pat) v cont = case pat of
+bindLetPat (WithSrcB sid pat) v cont = case pat of
UPatBinder b -> getDistinct >>= \Distinct -> extendSubst (b @> atomVarName v) cont
UPatProd ps -> do
let n = nestLength ps
case getType v of
TyCon (ProdType ts) | length ts == n -> return ()
- ty -> throw $ PatTypeErr "product type" (pprint ty)
+ ty -> throw sid $ PatTypeErr "product type" (pprint ty)
xs <- forM (iota n) \i -> proj i (toAtom v) >>= emitInline
bindLetPats ps xs cont
UPatDepPair (PairB p1 p2) -> do
case getType v of
TyCon (DepPairTy _) -> return ()
- ty -> throw $ PatTypeErr "dependent pair" (pprint ty)
+ ty -> throw sid $ PatTypeErr "dependent pair" (pprint ty)
-- XXX: we're careful here to reduce the projection because of the dependent
-- types. We do the same in the `UPatCon` case.
x1 <- reduceProj 0 (toAtom v) >>= emitInline
@@ -1586,16 +1598,16 @@ bindLetPat (WithSrcB _ pat) v cont = case pat of
case cons of
ADTCons [DataConDef _ _ _ idxss] -> do
when (length idxss /= nestLength ps) $
- throw $ PatternArityErr (length idxss) (nestLength ps)
+ throw sid $ PatternArityErr (length idxss) (nestLength ps)
void $ inferParams (getType $ toAtom v) dataDefName
xs <- forM idxss \idxs -> applyProjectionsReduced idxs (toAtom v) >>= emitInline
bindLetPats ps xs cont
- _ -> throw SumTypeCantFail
+ _ -> throw sid SumTypeCantFail
UPatTable ps -> do
let n = fromIntegral (nestLength ps) :: Word32
case getType v of
TyCon (TabPi (TabPiType _ (_:>FinConst n') _)) | n == n' -> return ()
- ty -> throw $ PatTypeErr ("Fin " ++ show n ++ " table") (pprint ty)
+ ty -> throw sid $ PatTypeErr ("Fin " ++ show n ++ " table") (pprint ty)
xs <- forM [0 .. n - 1] \i -> do
emitToVar =<< mkTabApp (toAtom v) (toAtom $ NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i))
bindLetPats ps xs cont
@@ -1610,28 +1622,28 @@ checkUType t = do
checkUParam :: Kind CoreIR o -> UType i -> InfererM i o (CAtom o)
checkUParam k uty =
- withReducibleEmissions msg $ withAllowedEffects Pure $ topDownExplicit (sink k) uty
+ withReducibleEmissions (getSrcId uty) msg $ withAllowedEffects Pure $ topDownExplicit (sink k) uty
where msg = CantReduceType $ pprint uty
-inferTabCon :: forall i o. Emits o => [UExpr i] -> InfererM i o (CAtom o)
-inferTabCon xs = do
+inferTabCon :: forall i o. Emits o => SrcId -> [UExpr i] -> InfererM i o (CAtom o)
+inferTabCon sid xs = do
let n = fromIntegral (length xs) :: Word32
let finTy = FinConst n
elemTy <- case xs of
- [] -> throw InferEmptyTable
+ [] -> throw sid InferEmptyTable
x:_ -> getType <$> bottomUp x
- ixTy <- asIxType finTy
+ ixTy <- asIxType sid finTy
let tabTy = ixTy ==> elemTy
xs' <- forM xs \x -> topDown elemTy x
let dTy = toType $ DataDictType elemTy
- Just dataDict <- toMaybeDict <$> trySynthTerm dTy Full
+ Just dataDict <- toMaybeDict <$> trySynthTerm sid dTy Full
emit $ TabCon (Just $ WhenIRE dataDict) tabTy xs'
-checkTabCon :: forall i o. Emits o => TabPiType CoreIR o -> [UExpr i] -> InfererM i o (CAtom o)
-checkTabCon tabTy@(TabPiType _ b elemTy) xs = do
+checkTabCon :: forall i o. Emits o => TabPiType CoreIR o -> SrcId -> [UExpr i] -> InfererM i o (CAtom o)
+checkTabCon tabTy@(TabPiType _ b elemTy) sid xs = do
let n = fromIntegral (length xs) :: Word32
let finTy = FinConst n
- expectEq (binderType b) finTy
+ expectEq sid (binderType b) finTy
xs' <- forM (enumerate xs) \(i, x) -> do
let i' = toAtom (NewtypeCon (FinCon (NatVal n)) (NatVal $ fromIntegral i)) :: CAtom o
elemTy' <- applySubst (b@>SubstVal i') elemTy
@@ -1643,22 +1655,22 @@ checkTabCon tabTy@(TabPiType _ b elemTy) xs = do
elemTy' <- applyRename (b@>binderName b') elemTy
let dTy = toType $ DataDictType elemTy'
return $ toType $ CorePiType ImplicitApp [Inferred Nothing Unify] (UnaryNest b') (EffTy Pure dTy)
- Just dataDict <- toMaybeDict <$> trySynthTerm dTy Full
+ Just dataDict <- toMaybeDict <$> trySynthTerm sid dTy Full
emit $ TabCon (Just $ WhenIRE dataDict) (TyCon (TabPi tabTy)) xs'
-addEffects :: EffectRow CoreIR o -> InfererM i o ()
-addEffects Pure = return ()
-addEffects eff = do
+addEffects :: SrcId -> EffectRow CoreIR o -> InfererM i o ()
+addEffects _ Pure = return ()
+addEffects sid eff = do
effsAllowed <- infEffects <$> getInfState
case checkExtends effsAllowed eff of
Success () -> return ()
- Failure _ -> expectEq (Eff effsAllowed) (Eff eff)
+ Failure _ -> expectEq sid (Eff effsAllowed) (Eff eff)
-getIxDict :: CType o -> InfererM i o (IxDict CoreIR o)
-getIxDict t = fromJust <$> toMaybeDict <$> trySynthTerm (toType $ IxDictType t) Full
+getIxDict :: SrcId -> CType o -> InfererM i o (IxDict CoreIR o)
+getIxDict sid t = fromJust <$> toMaybeDict <$> trySynthTerm sid (toType $ IxDictType t) Full
-asIxType :: CType o -> InfererM i o (IxType CoreIR o)
-asIxType ty = IxType ty <$> getIxDict ty
+asIxType :: SrcId -> CType o -> InfererM i o (IxType CoreIR o)
+asIxType sid ty = IxType ty <$> getIxDict sid ty
-- === Solver ===
@@ -1674,8 +1686,8 @@ lookupSolverSubst (SolverSubst m) name =
applyConstraint :: Constraint o -> SolverM i o ()
applyConstraint = \case
- TypeConstraint t1 t2 -> constrainEq t1 t2
- EffectConstraint r1 r2' -> do
+ TypeConstraint sid t1 t2 -> constrainEq sid t1 t2
+ EffectConstraint sid r1 r2' -> do
-- r1 shouldn't have inference variables. And we can't infer anything about
-- any inference variables in r2's explicit effects because we don't know
-- how they line up with r1's. So this is just about figuring out r2's tail.
@@ -1683,7 +1695,7 @@ applyConstraint = \case
let msg = DisallowedEffects (pprint r1) (pprint r2)
case checkExtends r1 r2 of
Success () -> return ()
- Failure _ -> searchFailureAsTypeErr msg do
+ Failure _ -> searchFailureAsTypeErr sid msg do
EffectRow effs1 t1 <- return r1
EffectRow effs2 (EffectRowTail v2) <- return r2
guard =<< isUnificationName (atomVarName v2)
@@ -1691,18 +1703,18 @@ applyConstraint = \case
let extras1 = effs1 `eSetDifference` effs2
extendSolution v2 (toAtom $ EffectRow extras1 t1)
-constrainEq :: ToAtom e CoreIR => e o -> e o -> SolverM i o ()
-constrainEq t1 t2 = do
+constrainEq :: ToAtom e CoreIR => SrcId -> e o -> e o -> SolverM i o ()
+constrainEq sid t1 t2 = do
t1' <- zonk $ toAtom t1
t2' <- zonk $ toAtom t2
msg <- liftEnvReaderM do
ab <- renameForPrinting $ PairE t1' t2'
return $ canonicalizeForPrinting ab \(Abs infVars (PairE t1Pretty t2Pretty)) ->
UnificationFailure (pprint t1Pretty) (pprint t2Pretty) (nestToList pprint infVars)
- void $ searchFailureAsTypeErr msg $ unify t1' t2'
+ void $ searchFailureAsTypeErr sid msg $ unify t1' t2'
-searchFailureAsTypeErr :: ToErr e => e -> SolverM i n a -> SolverM i n a
-searchFailureAsTypeErr msg cont = cont <|> throw msg
+searchFailureAsTypeErr :: ToErr e => SrcId -> e -> SolverM i n a -> SolverM i n a
+searchFailureAsTypeErr sid msg cont = cont <|> throw sid msg
{-# INLINE searchFailureAsTypeErr #-}
class AlphaEqE e => Unifiable (e::E) where
@@ -1933,22 +1945,25 @@ withFreshSkolemName ty cont = diffStateT1 \s -> do
(ans, diff) <- runDiffStateT1 (sink s) do
v <- toAtomVar $ binderName b
ans <- cont v >>= zonk
- liftHoistExcept $ hoist b ans
- diff' <- liftHoistExcept $ hoist b diff
- return (ans, diff')
+ case hoist b ans of
+ HoistSuccess ans' -> return ans'
+ HoistFailure _ -> empty
+ case hoist b diff of
+ HoistSuccess diff' -> return (ans, diff')
+ HoistFailure _ -> empty
{-# INLINE withFreshSkolemName #-}
extendSolution :: CAtomVar n -> CAtom n -> SolverM i n ()
extendSolution (AtomVar v _) t =
isUnificationName v >>= \case
True -> do
- when (v `isFreeIn` t) $ throw $ OccursCheckFailure (pprint v) (pprint t)
+ when (v `isFreeIn` t) solverFail -- occurs check
-- When we unify under a pi binder we replace its occurrences with a
-- skolem variable. We don't want to unify with terms containing these
-- variables because that would mean inferring dependence, which is a can
-- of worms.
forM_ (freeAtomVarsList t) \fv ->
- whenM (isSkolemName fv) $ throw CantUnifySkolem
+ whenM (isSkolemName fv) solverFail -- can't unify with skolems
addConstraint v t
False -> empty
@@ -2019,7 +2034,9 @@ generalizeDictRec targetTy (DictCon dict) = case dict of
InstanceDef _ roleExpls bs _ _ <- lookupInstanceDef instanceName
liftSolverM $ generalizeInstanceArgs roleExpls bs args \args' -> do
d <- mkInstanceDict (sink instanceName) args'
- constrainEq (sink $ toAtom targetTy) (toAtom $ getType d)
+ -- We use rootSrcId here because we only call this after type inference so
+ -- precise source info isn't needed.
+ constrainEq rootSrcId (sink $ toAtom targetTy) (toAtom $ getType d)
return d
IxFin _ -> do
TyCon (DictTy (IxDictType (TyCon (NewtypeTyCon (Fin n))))) <- return targetTy
@@ -2065,14 +2082,14 @@ emitInstanceDef instanceDef@(InstanceDef className _ _ _ _) = do
emitBinding (getNameHint className) $ InstanceBinding instanceDef ty
-- main entrypoint to dictionary synthesizer
-trySynthTerm :: CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
-trySynthTerm ty reqMethodAccess = do
+trySynthTerm :: SrcId -> CType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
+trySynthTerm sid ty reqMethodAccess = do
hasInferenceVars ty >>= \case
- True -> throw $ CantSynthInfVars $ pprint ty
+ True -> throw sid $ CantSynthInfVars $ pprint ty
False -> withVoidSubst do
synthTy <- liftExcept $ typeAsSynthType ty
- synthTerm synthTy reqMethodAccess
- <|> (throw $ CantSynthDict $ pprint ty)
+ synthTerm sid synthTy reqMethodAccess
+ <|> (throw sid $ CantSynthDict $ pprint ty)
{-# SCC trySynthTerm #-}
hasInferenceVars :: (EnvReader m, HoistableE e) => e n -> m n Bool
@@ -2159,11 +2176,11 @@ getSuperclassClosurePure env givens newGivens =
forM (enumerate superclasses) \(i, _) -> do
reduceSuperclassProj i $ fromJust (toMaybeDict synthExpr)
-synthTerm :: SynthType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
-synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
+synthTerm :: SrcId -> SynthType n -> RequiredMethodAccess -> InfererM i n (SynthAtom n)
+synthTerm sid targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
SynthPiType (expls, ab) -> do
ab' <- withFreshBindersInf expls ab \bs' targetTy' -> do
- Abs bs' <$> synthTerm (SynthDictType targetTy') reqMethodAccess
+ Abs bs' <$> synthTerm sid (SynthDictType targetTy') reqMethodAccess
Abs bs' synthExpr <- return ab'
let piTy = CorePiType ImplicitApp expls bs' (EffTy Pure (getType synthExpr))
let lamExpr = LamExpr bs' (Atom synthExpr)
@@ -2171,10 +2188,10 @@ synthTerm targetTy reqMethodAccess = confuseGHC >>= \_ -> case targetTy of
SynthDictType dictTy -> case dictTy of
IxDictType (TyCon (NewtypeTyCon (Fin n))) -> return $ toAtom $ IxFin n
DataDictType t -> do
- void (synthDictForData dictTy <|> synthDictFromGiven dictTy)
+ void (synthDictForData sid dictTy <|> synthDictFromGiven sid dictTy)
return $ toAtom $ DataData t
_ -> do
- dict <- synthDictFromInstance dictTy <|> synthDictFromGiven dictTy
+ dict <- synthDictFromInstance sid dictTy <|> synthDictFromGiven sid dictTy
case dict of
Con (DictConAtom (InstanceDict _ instanceName _)) -> do
isReqMethodAccessAllowed <- reqMethodAccess `isMethodAccessAllowedBy` instanceName
@@ -2194,8 +2211,8 @@ isMethodAccessAllowedBy access instanceName = do
Full -> return $ numClassMethods == numInstanceMethods
Partial numReqMethods -> return $ numReqMethods <= numInstanceMethods
-synthDictFromGiven :: DictType n -> InfererM i n (SynthAtom n)
-synthDictFromGiven targetTy = do
+synthDictFromGiven :: SrcId -> DictType n -> InfererM i n (SynthAtom n)
+synthDictFromGiven sid targetTy = do
givens <- ((HM.elems . fromGivens) <$> getGivens)
asum $ givens <&> \given -> do
case getSynthType given of
@@ -2203,15 +2220,15 @@ synthDictFromGiven targetTy = do
guard =<< alphaEq targetTy givenDictTy
return given
SynthPiType givenPiTy -> typeErrAsSearchFailure do
- args <- instantiateSynthArgs targetTy givenPiTy
+ args <- instantiateSynthArgs sid targetTy givenPiTy
reduceInstantiateGiven given args
-synthDictFromInstance :: DictType n -> InfererM i n (SynthAtom n)
-synthDictFromInstance targetTy = do
+synthDictFromInstance :: SrcId -> DictType n -> InfererM i n (SynthAtom n)
+synthDictFromInstance sid targetTy = do
instances <- getInstanceDicts targetTy
asum $ instances <&> \candidate -> typeErrAsSearchFailure do
CorePiType _ expls bs (EffTy _ (TyCon (DictTy candidateTy))) <- lookupInstanceTy candidate
- args <- instantiateSynthArgs targetTy (expls, Abs bs candidateTy)
+ args <- instantiateSynthArgs sid targetTy (expls, Abs bs candidateTy)
return $ toAtom $ InstanceDict (toType targetTy) candidate args
getInstanceDicts :: EnvReader m => DictType n -> m n [InstanceName n]
@@ -2230,11 +2247,11 @@ addInstanceSynthCandidate className maybeBuiltin instanceName = do
Just Data -> mempty
emitLocalModuleEnv $ mempty {envSynthCandidates = sc}
-instantiateSynthArgs :: DictType n -> SynthPiType n -> InfererM i n [CAtom n]
-instantiateSynthArgs target (expls, synthPiTy) = do
- liftM fromListE $ withReducibleEmissions CantReduceDict do
+instantiateSynthArgs :: SrcId -> DictType n -> SynthPiType n -> InfererM i n [CAtom n]
+instantiateSynthArgs sid target (expls, synthPiTy) = do
+ liftM fromListE $ withReducibleEmissions sid CantReduceDict do
bsConstrained <- buildConstraints (sink synthPiTy) \_ resultTy -> do
- return [TypeConstraint (TyCon $ DictTy $ sink target) (TyCon $ DictTy resultTy)]
+ return [TypeConstraint sid (TyCon $ DictTy $ sink target) (TyCon $ DictTy resultTy)]
ListE <$> inferMixedArgs "dict" expls bsConstrained emptyMixedArgs
emptyMixedArgs :: MixedArgs (CAtom n)
@@ -2245,11 +2262,11 @@ typeErrAsSearchFailure cont = cont `catchErr` \case
TypeErr _ -> empty
e -> throwErr e
-synthDictForData :: forall i n. DictType n -> InfererM i n (SynthAtom n)
-synthDictForData dictTy@(DataDictType ty) = case ty of
+synthDictForData :: forall i n. SrcId -> DictType n -> InfererM i n (SynthAtom n)
+synthDictForData sid dictTy@(DataDictType ty) = case ty of
-- TODO Deduplicate vs CheckType.checkDataLike
-- The "Stuck" case is different
- StuckTy _ _ -> synthDictFromGiven dictTy
+ StuckTy _ _ -> synthDictFromGiven sid dictTy
TyCon con -> case con of
TabPi (TabPiType _ b eltTy) -> recurBinder (Abs b eltTy) >> success
DepPairTy (DepPairType _ b@(_:>l) r) -> do
@@ -2264,16 +2281,16 @@ synthDictForData dictTy@(DataDictType ty) = case ty of
HeapType -> success
_ -> notData
where
- recur ty' = synthDictForData $ DataDictType ty'
+ recur ty' = synthDictForData sid $ DataDictType ty'
recurBinder :: Abs CBinder CType n -> InfererM i n (SynthAtom n)
recurBinder (Abs b body) =
withFreshBinderInf noHint Explicit (binderType b) \b' -> do
body' <- applyRename (b@>binderName b') body
- ans <- synthDictForData $ DataDictType (toType body')
+ ans <- synthDictForData sid $ DataDictType (toType body')
return $ ignoreHoistFailure $ hoist b' ans
notData = empty
success = return $ toAtom $ DataData ty
-synthDictForData dictTy = error $ "Malformed Data dictTy " ++ pprint dictTy
+synthDictForData _ dictTy = error $ "Malformed Data dictTy " ++ pprint dictTy
instance GenericE Givens where
type RepE Givens = HashMapE (EKey SynthType) SynthAtom
@@ -2329,7 +2346,7 @@ checkFFIFunTypeM _ = error "expected at least one argument"
checkScalar :: (IRRep r, Fallible m) => Type r n -> m BaseType
checkScalar (BaseTy ty) = return ty
-checkScalar ty = throw $ FFIArgTyNotScalar $ pprint ty
+checkScalar ty = throw rootSrcId $ FFIArgTyNotScalar $ pprint ty
checkScalarOrPairType :: (IRRep r, Fallible m) => Type r n -> m [BaseType]
checkScalarOrPairType (PairTy a b) = do
@@ -2337,7 +2354,7 @@ checkScalarOrPairType (PairTy a b) = do
tys2 <- checkScalarOrPairType b
return $ tys1 ++ tys2
checkScalarOrPairType (BaseTy ty) = return [ty]
-checkScalarOrPairType ty = throw $ FFIResultTyErr $ pprint ty
+checkScalarOrPairType ty = throw rootSrcId $ FFIResultTyErr $ pprint ty
-- === instances ===
@@ -2417,14 +2434,16 @@ instance RenameE SynthType
instance SubstE AtomSubstVal SynthType
instance GenericE Constraint where
- type RepE Constraint = EitherE
- (PairE CType CType)
- (PairE (EffectRow CoreIR) (EffectRow CoreIR))
- fromE (TypeConstraint t1 t2) = LeftE (PairE t1 t2)
- fromE (EffectConstraint e1 e2) = RightE (PairE e1 e2)
+ type RepE Constraint = PairE
+ (LiftE SrcId)
+ (EitherE
+ (PairE CType CType)
+ (PairE (EffectRow CoreIR) (EffectRow CoreIR)))
+ fromE (TypeConstraint sid t1 t2) = LiftE sid `PairE` LeftE (PairE t1 t2)
+ fromE (EffectConstraint sid e1 e2) = LiftE sid `PairE` RightE (PairE e1 e2)
{-# INLINE fromE #-}
- toE (LeftE (PairE t1 t2)) = TypeConstraint t1 t2
- toE (RightE (PairE e1 e2)) = EffectConstraint e1 e2
+ toE (LiftE sid `PairE` LeftE (PairE t1 t2)) = TypeConstraint sid t1 t2
+ toE (LiftE sid `PairE` RightE (PairE e1 e2)) = EffectConstraint sid e1 e2
{-# INLINE toE #-}
instance SinkableE Constraint
diff --git a/src/lib/Lexing.hs b/src/lib/Lexing.hs
index 111027ff..e8ad7c7f 100644
--- a/src/lib/Lexing.hs
+++ b/src/lib/Lexing.hs
@@ -44,7 +44,7 @@ type Parser = StateT ParseCtx (Parsec Void Text)
parseit :: Text -> Parser a -> Except a
parseit s p = case parse (fst <$> runStateT p initParseCtx) "" s of
- Left e -> throw $ MiscParseErr $ errorBundlePretty e
+ Left e -> throw rootSrcId $ MiscParseErr $ errorBundlePretty e
Right x -> return x
mustParseit :: Text -> Parser a -> a
diff --git a/src/lib/Name.hs b/src/lib/Name.hs
index 4f025384..9aa9402c 100644
--- a/src/lib/Name.hs
+++ b/src/lib/Name.hs
@@ -2755,9 +2755,9 @@ canonicalizeForPrinting e cont = do
pprintCanonicalized :: (HoistableE e, RenameE e, PrettyE e) => e n -> String
pprintCanonicalized e = canonicalizeForPrinting e \e' -> pprint e'
-liftHoistExcept :: Fallible m => HoistExcept a -> m a
-liftHoistExcept (HoistSuccess x) = return x
-liftHoistExcept (HoistFailure vs) = throw $ EscapedNameErr $ map pprint vs
+liftHoistExcept :: Fallible m => SrcId -> HoistExcept a -> m a
+liftHoistExcept _ (HoistSuccess x) = return x
+liftHoistExcept sid (HoistFailure vs) = throw sid $ EscapedNameErr $ map pprint vs
ignoreHoistFailure :: HasCallStack => HoistExcept a -> a
ignoreHoistFailure (HoistSuccess x) = x
@@ -2845,10 +2845,11 @@ exchangeBs (PairB b1 b2) =
partitionBinders
:: forall b b1 b2 m n l
- . (SinkableB b2, HoistableB b1, BindsNames b2, Fallible m, Distinct l) => Nest b n l
+ . (SinkableB b2, HoistableB b1, BindsNames b2, Fallible m, Distinct l)
+ => SrcId -> Nest b n l
-> (forall n' l'. b n' l' -> m (EitherB b1 b2 n' l'))
-> m (PairB (Nest b1) (Nest b2) n l)
-partitionBinders bs assignBinder = go bs where
+partitionBinders sid bs assignBinder = go bs where
go :: Distinct l' => Nest b n' l' -> m (PairB (Nest b1) (Nest b2) n' l')
go = \case
Empty -> return $ PairB Empty Empty
@@ -2859,7 +2860,7 @@ partitionBinders bs assignBinder = go bs where
RightB b2 -> withSubscopeDistinct bs2
case exchangeBs (PairB b2 bs1) of
HoistSuccess (PairB bs1' b2') -> return $ PairB bs1' (Nest b2' bs2)
- HoistFailure vs -> throw $ EscapedNameErr $ map pprint vs
+ HoistFailure vs -> throw sid $ EscapedNameErr $ map pprint vs
-- NameBinder has no free vars, so there's no risk associated with hoisting.
-- The scope is completely distinct, so their exchange doesn't create any accidental
diff --git a/src/lib/QueryType.hs b/src/lib/QueryType.hs
index acbff02c..6229a1e8 100644
--- a/src/lib/QueryType.hs
+++ b/src/lib/QueryType.hs
@@ -28,11 +28,6 @@ import PPrint
import QueryTypePure
import CheapReduction
-sourceNameType :: (EnvReader m, Fallible1 m) => SourceName -> m n (Type CoreIR n)
-sourceNameType v = do
- lookupSourceMap v >>= \case
- Nothing -> throw $ UnboundVarErr $ pprint v
- Just uvar -> getUVarType uvar
-- === Exposed helpers for querying types and effects ===
diff --git a/src/lib/Runtime.hs b/src/lib/Runtime.hs
index 10201909..011604d8 100644
--- a/src/lib/Runtime.hs
+++ b/src/lib/Runtime.hs
@@ -72,7 +72,7 @@ checkedCallFunPtr :: FD -> Ptr () -> Ptr () -> DexExecutable -> IO ()
checkedCallFunPtr fd argsPtr resultPtr fPtr = do
let (CInt fd') = fdFD fd
exitCode <- callFunPtr fPtr fd' argsPtr resultPtr
- unless (exitCode == 0) $ throw RuntimeErr
+ unless (exitCode == 0) $ throw rootSrcId RuntimeErr
withPipeToLogger :: PassLogger -> (FD -> IO a) -> IO a
withPipeToLogger logger writeAction = do
diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs
index 1fcaa73d..d5420dab 100644
--- a/src/lib/SourceRename.hs
+++ b/src/lib/SourceRename.hs
@@ -98,20 +98,20 @@ class SourceRenamableB (b :: B) where
-> m o a
instance SourceRenamableE (SourceNameOr UVar) where
- sourceRenameE (SourceName pos sourceName) =
- InternalName pos sourceName <$> lookupSourceName sourceName
+ sourceRenameE (SourceName sid sourceName) =
+ InternalName sid sourceName <$> lookupSourceName sid sourceName
sourceRenameE _ = error "Shouldn't be source-renaming internal names"
-lookupSourceName :: Renamer m => SourceName -> m n (UVar n)
-lookupSourceName v = do
+lookupSourceName :: Renamer m => SrcId -> SourceName -> m n (UVar n)
+lookupSourceName sid v = do
sm <- askSourceMap
case lookupSourceMapPure sm v of
- [] -> throw $ UnboundVarErr $ pprint v
+ [] -> throw sid $ UnboundVarErr $ pprint v
LocalVar v' : _ -> return v'
[ModuleVar _ maybeV] -> case maybeV of
Just v' -> return v'
- Nothing -> throw $ VarDefErr $ pprint v
- vs -> throw $ AmbiguousVarErr (pprint v) (map wherePretty vs)
+ Nothing -> throw sid $ VarDefErr $ pprint v
+ vs -> throw sid $ AmbiguousVarErr (pprint v) (map wherePretty vs)
where
wherePretty :: SourceNameDef n -> String
wherePretty (ModuleVar mname _) = case mname of
@@ -122,24 +122,24 @@ lookupSourceName v = do
error "shouldn't be possible because module vars can't shadow local ones"
instance SourceRenamableE (SourceNameOr (Name (AtomNameC CoreIR))) where
- sourceRenameE (SourceName pos sourceName) = do
- lookupSourceName sourceName >>= \case
- UAtomVar v -> return $ InternalName pos sourceName v
- _ -> throw $ NotAnOrdinaryVar $ pprint sourceName
+ sourceRenameE (SourceName sid sourceName) = do
+ lookupSourceName sid sourceName >>= \case
+ UAtomVar v -> return $ InternalName sid sourceName v
+ _ -> throw sid $ NotAnOrdinaryVar $ pprint sourceName
sourceRenameE _ = error "Shouldn't be source-renaming internal names"
instance SourceRenamableE (SourceNameOr (Name DataConNameC)) where
- sourceRenameE (SourceName pos sourceName) = do
- lookupSourceName sourceName >>= \case
- UDataConVar v -> return $ InternalName pos sourceName v
- _ -> throw $ NotADataCon $ pprint sourceName
+ sourceRenameE (SourceName sid sourceName) = do
+ lookupSourceName sid sourceName >>= \case
+ UDataConVar v -> return $ InternalName sid sourceName v
+ _ -> throw sid $ NotADataCon $ pprint sourceName
sourceRenameE _ = error "Shouldn't be source-renaming internal names"
instance SourceRenamableE (SourceNameOr (Name ClassNameC)) where
- sourceRenameE (SourceName pos sourceName) = do
- lookupSourceName sourceName >>= \case
- UClassVar v -> return $ InternalName pos sourceName v
- _ -> throw $ NotAClassName $ pprint sourceName
+ sourceRenameE (SourceName sid sourceName) = do
+ lookupSourceName sid sourceName >>= \case
+ UClassVar v -> return $ InternalName sid sourceName v
+ _ -> throw sid $ NotAClassName $ pprint sourceName
sourceRenameE _ = error "Shouldn't be source-renaming internal names"
instance SourceRenamableE (SourceNameOr (Name c)) => SourceRenamableE (SourceOrInternalName c) where
@@ -148,8 +148,8 @@ instance SourceRenamableE (SourceNameOr (Name c)) => SourceRenamableE (SourceOrI
instance (SourceRenamableE e, SourceRenamableB b) => SourceRenamableE (Abs b e) where
sourceRenameE (Abs b e) = sourceRenameB b \b' -> Abs b' <$> sourceRenameE e
-instance SourceRenamableB (UBinder' (AtomNameC CoreIR)) where
- sourceRenameB b cont = sourceRenameUBinder' UAtomVar b cont
+instance SourceRenamableB (UBinder (AtomNameC CoreIR)) where
+ sourceRenameB b cont = sourceRenameUBinder UAtomVar b cont
instance SourceRenamableE UAnn where
sourceRenameE UNoAnn = return UNoAnn
@@ -161,8 +161,8 @@ instance SourceRenamableB UAnnBinder where
cs' <- mapM sourceRenameE cs
sourceRenameB b \b' -> cont $ UAnnBinder expl b' ann' cs'
-instance SourceRenamableE UExpr' where
- sourceRenameE expr = setMayShadow True case expr of
+instance SourceRenamableE UExpr where
+ sourceRenameE (WithSrcE sid expr) = liftM (WithSrcE sid) $ setMayShadow True case expr of
UVar v -> UVar <$> sourceRenameE v
ULit l -> return $ ULit l
ULam lam -> ULam <$> sourceRenameE lam
@@ -211,12 +211,6 @@ instance SourceRenamableE UEffect where
sourceRenameE UExceptionEffect = return UExceptionEffect
sourceRenameE UIOEffect = return UIOEffect
-instance SourceRenamableE a => SourceRenamableE (WithSrcE a) where
- sourceRenameE (WithSrcE pos e) = WithSrcE pos <$> sourceRenameE e
-
-instance SourceRenamableB a => SourceRenamableB (WithSrcB a) where
- sourceRenameB (WithSrcB pos b) cont = sourceRenameB b \b' -> cont $ WithSrcB pos b'
-
instance SourceRenamableB UTopDecl where
sourceRenameB decl cont = case decl of
ULocalDecl d -> sourceRenameB d \d' -> cont $ ULocalDecl d'
@@ -244,15 +238,17 @@ instance SourceRenamableB UTopDecl where
sourceRenameB instanceName \instanceName' ->
cont $ UInstance className' conditions' params' methodDefs' instanceName' expl
-instance SourceRenamableB UDecl' where
- sourceRenameB decl cont = case decl of
+instance SourceRenamableB UDecl where
+ sourceRenameB (WithSrcB sid decl) cont = case decl of
ULet ann pat ty expr -> do
expr' <- sourceRenameE expr
ty' <- mapM sourceRenameE ty
sourceRenameB pat \pat' ->
- cont $ ULet ann pat' ty' expr'
- UExprDecl e -> cont =<< (UExprDecl <$> sourceRenameE e)
- UPass -> cont UPass
+ cont $ WithSrcB sid $ ULet ann pat' ty' expr'
+ UExprDecl e -> do
+ e' <- UExprDecl <$> sourceRenameE e
+ cont $ WithSrcB sid e'
+ UPass -> cont $ WithSrcB sid UPass
instance SourceRenamableE ULamExpr where
sourceRenameE (ULamExpr args expl effs resultTy body) =
@@ -262,11 +258,11 @@ instance SourceRenamableE ULamExpr where
<*> mapM sourceRenameE resultTy
<*> sourceRenameE body
-instance SourceRenamableE UBlock' where
- sourceRenameE (UBlock decls result) =
+instance SourceRenamableE UBlock where
+ sourceRenameE (WithSrcE sid (UBlock decls result)) =
sourceRenameB decls \decls' -> do
result' <- sourceRenameE result
- return $ UBlock decls' result'
+ return $ WithSrcE sid $ UBlock decls' result'
instance SourceRenamableB UnitB where
sourceRenameB UnitB cont = cont UnitB
@@ -294,31 +290,24 @@ sourceRenameUBinderNest asUVar (Nest b bs) cont =
sourceRenameUBinderNest asUVar bs \bs' ->
cont $ Nest b' bs'
-sourceRenameUBinder' :: (Color c, Distinct o, Renamer m)
- => (forall l. Name c l -> UVar l)
- -> UBinder' c i i'
- -> (forall o'. DExt o o' => UBinder' c o o' -> m o' a)
- -> m o a
-sourceRenameUBinder' asUVar ubinder cont = case ubinder of
+sourceRenameUBinder
+ :: (Color c, Distinct o, Renamer m)
+ => (forall l. Name c l -> UVar l)
+ -> UBinder c i i'
+ -> (forall o'. DExt o o' => UBinder c o o' -> m o' a)
+ -> m o a
+sourceRenameUBinder asUVar (WithSrcB sid ubinder) cont = case ubinder of
UBindSource b -> do
SourceMap sm <- askSourceMap
mayShadow <- askMayShadow
let shadows = M.member b sm
- when (not mayShadow && shadows) $ throw (RepeatedVarErr $ pprint b)
+ when (not mayShadow && shadows) $ throw sid $ RepeatedVarErr $ pprint b
withFreshM (getNameHint b) \freshName -> do
Distinct <- getDistinct
extendSourceMap b (asUVar $ binderName freshName) $
- cont $ UBind b freshName
+ cont $ WithSrcB sid $ UBind b freshName
UBind _ _ -> error "Shouldn't be source-renaming internal names"
- UIgnore -> cont $ UIgnore
-
-sourceRenameUBinder :: (Color c, Distinct o, Renamer m)
- => (forall l. Name c l -> UVar l)
- -> UBinder c i i'
- -> (forall o'. DExt o o' => UBinder c o o' -> m o' a)
- -> m o a
-sourceRenameUBinder asUVar (WithSrcB sid ubinder) cont =
- sourceRenameUBinder' asUVar ubinder \ubinder' -> cont (WithSrcB sid ubinder')
+ UIgnore -> cont $ WithSrcB sid $ UIgnore
instance SourceRenamableE UDataDef where
sourceRenameE (UDataDef tyConName paramBs dataCons) = do
@@ -356,11 +345,11 @@ instance SourceRenamableE e => SourceRenamableE (ListE e) where
instance SourceRenamableE UnitE where
sourceRenameE UnitE = return UnitE
-instance SourceRenamableE UMethodDef' where
- sourceRenameE (UMethodDef ~(SourceName pos v) expr) = do
- lookupSourceName v >>= \case
- UMethodVar v' -> UMethodDef (InternalName pos v v') <$> sourceRenameE expr
- _ -> throw $ NotAMethodName $ pprint v
+instance SourceRenamableE UMethodDef where
+ sourceRenameE (WithSrcE sid ((UMethodDef ~(SourceName vSid v) expr))) = WithSrcE sid <$> do
+ lookupSourceName vSid v >>= \case
+ UMethodVar v' -> UMethodDef (InternalName vSid v v') <$> sourceRenameE expr
+ _ -> throw vSid $ NotAMethodName $ pprint v
instance SourceRenamableB b => SourceRenamableB (Nest b) where
sourceRenameB (Nest b bs) cont =
@@ -383,32 +372,33 @@ class SourceRenamablePat (pat::B) where
-> (forall o'. DExt o o' => SiblingSet -> pat o o' -> m o' a)
-> m o a
-instance SourceRenamablePat (UBinder' (AtomNameC CoreIR)) where
- sourceRenamePat sibs ubinder cont = do
+instance SourceRenamablePat (UBinder (AtomNameC CoreIR)) where
+ sourceRenamePat sibs (WithSrcB sid ubinder) cont = do
newSibs <- case ubinder of
UBindSource b -> do
- when (S.member b sibs) $ throw $ RepeatedPatVarErr $ pprint b
+ when (S.member b sibs) $ throw sid $ RepeatedPatVarErr $ pprint b
return $ S.singleton b
UIgnore -> return mempty
UBind _ _ -> error "Shouldn't be source-renaming internal names"
- sourceRenameB ubinder \ubinder' ->
+ sourceRenameB (WithSrcB sid ubinder) \ubinder' ->
cont (sibs <> newSibs) ubinder'
-instance SourceRenamablePat UPat' where
- sourceRenamePat sibs pat cont = case pat of
- UPatBinder b -> sourceRenamePat sibs b \sibs' b' -> cont sibs' $ UPatBinder b'
+instance SourceRenamablePat UPat where
+ sourceRenamePat sibs (WithSrcB sid pat) cont = case pat of
+ UPatBinder b -> sourceRenamePat sibs b \sibs' b' ->
+ cont sibs' $ WithSrcB sid $ UPatBinder b'
UPatCon con bs -> do
-- TODO Deduplicate this against the code for sourceRenameE of
-- the SourceName case of SourceNameOr
con' <- sourceRenameE con
sourceRenamePat sibs bs \sibs' bs' ->
- cont sibs' $ UPatCon con' bs'
+ cont sibs' $ WithSrcB sid $ UPatCon con' bs'
UPatDepPair (PairB p1 p2) ->
sourceRenamePat sibs p1 \sibs' p1' ->
sourceRenamePat sibs' p2 \sibs'' p2' ->
- cont sibs'' $ UPatDepPair $ PairB p1' p2'
- UPatProd bs -> sourceRenamePat sibs bs \sibs' bs' -> cont sibs' $ UPatProd bs'
- UPatTable ps -> sourceRenamePat sibs ps \sibs' ps' -> cont sibs' $ UPatTable ps'
+ cont sibs'' $ WithSrcB sid $ UPatDepPair $ PairB p1' p2'
+ UPatProd bs -> sourceRenamePat sibs bs \sibs' bs' -> cont sibs' $ WithSrcB sid $ UPatProd bs'
+ UPatTable ps -> sourceRenamePat sibs ps \sibs' ps' -> cont sibs' $ WithSrcB sid $ UPatTable ps'
instance SourceRenamablePat UnitB where
sourceRenamePat sibs UnitB cont = cont sibs UnitB
@@ -429,11 +419,6 @@ instance (SourceRenamablePat p1, SourceRenamablePat p2)
sourceRenamePat sibs p \sibs' p' ->
cont sibs' $ RightB p'
-instance SourceRenamablePat p => SourceRenamablePat (WithSrcB p) where
- sourceRenamePat sibs (WithSrcB pos pat) cont = do
- sourceRenamePat sibs pat \sibs' pat' ->
- cont sibs' $ WithSrcB pos pat'
-
instance SourceRenamablePat p => SourceRenamablePat (Nest p) where
sourceRenamePat sibs (Nest b bs) cont =
sourceRenamePat sibs b \sibs' b' ->
@@ -441,7 +426,7 @@ instance SourceRenamablePat p => SourceRenamablePat (Nest p) where
cont sibs'' $ Nest b' bs'
sourceRenamePat sibs Empty cont = cont sibs Empty
-instance SourceRenamableB UPat' where
+instance SourceRenamableB UPat where
sourceRenameB pat cont =
sourceRenamePat mempty pat \_ pat' -> cont pat'
diff --git a/src/lib/TopLevel.hs b/src/lib/TopLevel.hs
index 47b132c3..5f0f84ea 100644
--- a/src/lib/TopLevel.hs
+++ b/src/lib/TopLevel.hs
@@ -263,7 +263,7 @@ evalSourceBlock' mname block = case sbContents block of
DeclareForeign fname (WithSrc _ dexName) cTy -> do
ty <- evalUType =<< parseExpr cTy
asFFIFunType ty >>= \case
- Nothing -> throw $ MiscMiscErr
+ Nothing -> throw rootSrcId $ MiscMiscErr
"FFI functions must be n-ary first order functions with the IO effect"
Just (impFunTy, naryPiTy) -> do
-- TODO: query linking stuff and check the function is actually available
@@ -275,15 +275,15 @@ evalSourceBlock' mname block = case sbContents block of
DeclareCustomLinearization fname zeros g -> do
expr <- parseExpr g
lookupSourceMap (withoutSrc fname) >>= \case
- Nothing -> throw $ UnboundVarErr $ pprint fname
+ Nothing -> throw rootSrcId $ UnboundVarErr $ pprint fname
Just (UAtomVar fname') -> do
lookupCustomRules fname' >>= \case
Nothing -> return ()
- Just _ -> throw $ MiscMiscErr
+ Just _ -> throw rootSrcId $ MiscMiscErr
$ pprint fname ++ " already has a custom linearization"
lookupAtomName fname' >>= \case
NoinlineFun _ _ -> return ()
- _ -> throw $ MiscMiscErr "Custom linearizations only apply to @noinline functions"
+ _ -> throw rootSrcId $ MiscMiscErr "Custom linearizations only apply to @noinline functions"
-- We do some special casing to avoid instantiating polymorphic functions.
impl <- case expr of
WithSrcE _ (UVar _) ->
@@ -296,17 +296,20 @@ evalSourceBlock' mname block = case sbContents block of
liftEnvReaderT (impl `checkTypeIs` linFunTy) >>= \case
Failure _ -> do
let implTy = getType impl
- throw $ MiscMiscErr $ unlines
+ throw rootSrcId $ MiscMiscErr $ unlines
[ "Expected the custom linearization to have type:" , "" , pprint linFunTy , ""
, "but it has type:" , "" , pprint implTy]
Success () -> return ()
updateTopEnv $ AddCustomRule fname' $ CustomLinearize nimplicit nexplicit zeros impl
- Just _ -> throw $ MiscMiscErr $ "Custom linearization can only be defined for functions"
- UnParseable _ s -> throw $ MiscParseErr s
+ Just _ -> throw rootSrcId $ MiscMiscErr $ "Custom linearization can only be defined for functions"
+ UnParseable _ s -> throw rootSrcId $ MiscParseErr s
Misc m -> case m of
GetNameType v -> do
- ty <- sourceNameType (withoutSrc v)
- logTop $ TextOut $ pprintCanonicalized ty
+ lookupSourceMap (withoutSrc v) >>= \case
+ Nothing -> throw rootSrcId $ UnboundVarErr $ pprint v
+ Just uvar -> do
+ ty <- getUVarType uvar
+ logTop $ TextOut $ pprintCanonicalized ty
ImportModule moduleName -> importModule moduleName
QueryEnv query -> void $ runEnvQuery query $> UnitE
ProseBlock _ -> return ()
@@ -327,11 +330,11 @@ runEnvQuery query = do
DumpSubst -> logTop $ TextOut $ pprint $ env
InternalNameInfo name ->
case lookupSubstFragRaw (fromRecSubst $ envDefs $ topEnv env) name of
- Nothing -> throw $ UnboundVarErr $ pprint name
+ Nothing -> throw rootSrcId $ UnboundVarErr $ pprint name
Just binding -> logTop $ TextOut $ pprint binding
SourceNameInfo name -> do
lookupSourceMap name >>= \case
- Nothing -> throw $ UnboundVarErr $ pprint name
+ Nothing -> throw rootSrcId $ UnboundVarErr $ pprint name
Just uvar -> do
logTop $ TextOut $ pprint uvar
info <- case uvar of
@@ -434,7 +437,7 @@ evalUModule (UModule name _ blocks) = do
importModule :: (Mut n, TopBuilder m, Fallible1 m) => ModuleSourceName -> m n ()
importModule name = do
lookupLoadedModule name >>= \case
- Nothing -> throw $ ModuleImportErr $ pprint name
+ Nothing -> throw rootSrcId $ ModuleImportErr $ pprint name
Just name' -> do
Module _ _ transImports' _ _ <- lookupModule name'
let importStatus = ImportStatus (S.singleton name')
@@ -693,7 +696,7 @@ loadModuleSource config moduleName = do
fsPaths <- liftIO $ traverse resolveBuiltinPath $ libPaths config
liftIO (findFile fsPaths fname) >>= \case
Just fpath -> return fpath
- Nothing -> throw $ CantFindModuleSource $ pprint moduleName
+ Nothing -> throw rootSrcId $ CantFindModuleSource $ pprint moduleName
resolveBuiltinPath = \case
LibBuiltinPath -> liftIO $ getDataFileName "lib"
LibDirectory dir -> return dir
@@ -832,14 +835,14 @@ getLinearizationType zeros = \case
Just tty -> case zeros of
InstantiateZeros -> return tty
SymbolicZeros -> symbolicTangentTy tty
- Nothing -> throw $ MiscMiscErr $ "No tangent type for: " ++ pprint t
+ Nothing -> throw rootSrcId $ MiscMiscErr $ "No tangent type for: " ++ pprint t
resultTanTy <- maybeTangentType resultTy' >>= \case
Just rtt -> return rtt
- Nothing -> throw $ MiscMiscErr $ "No tangent type for: " ++ pprint resultTy'
+ Nothing -> throw rootSrcId $ MiscMiscErr $ "No tangent type for: " ++ pprint resultTy'
let tanFunTy = toType $ Pi $ nonDepPiType argTanTys Pure resultTanTy
let fullTy = CorePiType ExplicitApp expls bs' $ EffTy Pure (PairTy resultTy' tanFunTy)
return (numIs, numEs, toType $ Pi fullTy)
- _ -> throw $ MiscMiscErr $ "Can't define a custom linearization for implicit or impure functions"
+ _ -> throw rootSrcId $ MiscMiscErr $ "Can't define a custom linearization for implicit or impure functions"
where
getNumImplicits :: Fallible m => [Explicitness] -> m (Int, Int)
getNumImplicits = \case
@@ -850,4 +853,4 @@ getLinearizationType zeros = \case
Inferred _ _ -> return (ni + 1, ne)
Explicit -> case ni of
0 -> return (0, ne + 1)
- _ -> throw $ MiscMiscErr "All implicit args must precede implicit args"
+ _ -> throw rootSrcId $ MiscMiscErr "All implicit args must precede implicit args"
diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs
index 87a6e676..b20a0e09 100644
--- a/src/lib/Types/Source.hs
+++ b/src/lib/Types/Source.hs
@@ -480,6 +480,14 @@ data WithSrcE (a::E) (n::S) = WithSrcE SrcId (a n)
data WithSrcB (binder::B) (n::S) (l::S) = WithSrcB SrcId (binder n l)
deriving (Show, Generic)
+instance HasSrcId (WithSrc a ) where getSrcId (WithSrc sid _ ) = sid
+instance HasSrcId (WithSrcs a ) where getSrcId (WithSrcs sid _ _) = sid
+instance HasSrcId (WithSrcE e n ) where getSrcId (WithSrcE sid _ ) = sid
+instance HasSrcId (WithSrcB b n l) where getSrcId (WithSrcB sid _ ) = sid
+
+instance HasSrcId (UAnnBinder n l) where
+ getSrcId (UAnnBinder _ b _ _) = getSrcId b
+
class HasSrcPos withSrc a | withSrc -> a where
srcPos :: withSrc -> SrcId
withoutSrc :: withSrc -> a
generated by cgit v1.2.3-70-g09d2 (git 2.46.0) at 2024-10-22 20:49:12 +0000