Skip to content

Commit

Permalink
Improve locations of error messages.
Browse files Browse the repository at this point in the history 
Fixes #1299
  • Loading branch information
@yav
yav committed Oct 29, 2021
1 parent 8f16776 commit 851ef89
Show file tree
Hide file tree
Showing 7 changed files with 94 additions and 59 deletions.
86 changes: 47 additions & 39 deletions src/Cryptol/TypeCheck/Infer.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,7 @@ import Data.List(partition)
import Data.Ratio(numerator,denominator)
import Data.Traversable(forM)
import Data.Function(on)
import Control.Monad(zipWithM,unless,foldM,forM_)
import Control.Monad(zipWithM,unless,foldM,forM_,mplus)



Expand Down Expand Up @@ -247,13 +247,14 @@ checkE expr tGoal =

P.ETuple es ->
do etys <- expectTuple (length es) tGoal
let mkTGoal n t = WithSource t (TypeOfTupleField n)
es' <- zipWithM checkE es (zipWith mkTGoal [1..] etys)
let mkTGoal n t e = WithSource t (TypeOfTupleField n) (getLoc e)
es' <- zipWithM checkE es (zipWith3 mkTGoal [1..] etys es)
return (ETuple es')

P.ERecord fs ->
do es <- expectRec fs tGoal
let checkField f (e,t) = checkE e (WithSource t (TypeOfRecordField f))
let checkField f (e,t) =
checkE e (WithSource t (TypeOfRecordField f) (getLoc e))
es' <- traverseRecordMap checkField es
return (ERec es')

Expand All @@ -262,19 +263,19 @@ checkE expr tGoal =
P.ESel e l ->
do let src = selSrc l
t <- newType src KType
e' <- checkE e (WithSource t src)
e' <- checkE e (WithSource t src (getLoc expr))
f <- newHasGoal l t (twsType tGoal)
return (hasDoSelect f e')

P.EList [] ->
do (len,a) <- expectSeq tGoal
expectFin 0 (WithSource len LenOfSeq)
expectFin 0 (WithSource len LenOfSeq (getLoc expr))
return (EList [] a)

P.EList es ->
do (len,a) <- expectSeq tGoal
expectFin (length es) (WithSource len LenOfSeq)
let checkElem e = checkE e (WithSource a TypeOfSeqElement)
expectFin (length es) (WithSource len LenOfSeq (getLoc expr))
let checkElem e = checkE e (WithSource a TypeOfSeqElement (getLoc e))
es' <- mapM checkElem es
return (EList es' a)

Expand Down Expand Up @@ -378,11 +379,12 @@ checkE expr tGoal =
(len,a) <- expectSeq tGoal

inferred <- smallest ts
ctrs <- unify (WithSource len LenOfSeq) inferred
ctrs <- unify (WithSource len LenOfSeq (getLoc expr)) inferred
newGoals CtComprehension ctrs

ds <- combineMaps dss
e' <- withMonoTypes ds (checkE e (WithSource a TypeOfSeqElement))
e' <- withMonoTypes ds (checkE e
(WithSource a TypeOfSeqElement (getLoc e)))
return (EComp len a e' mss')
where
-- the renamer should have made these checks already?
Expand All @@ -407,12 +409,13 @@ checkE expr tGoal =
P.EApp e1 e2 ->
do let argSrc = TypeOfArg noArgDescr
t1 <- newType argSrc KType
e1' <- checkE e1 (WithSource (tFun t1 (twsType tGoal)) FunApp)
e2' <- checkE e2 (WithSource t1 argSrc)
e1' <- checkE e1
(WithSource (tFun t1 (twsType tGoal)) FunApp (getLoc e1))
e2' <- checkE e2 (WithSource t1 argSrc (getLoc e2))
return (EApp e1' e2')

P.EIf e1 e2 e3 ->
do e1' <- checkE e1 (WithSource tBit TypeOfIfCondExpr)
do e1' <- checkE e1 (WithSource tBit TypeOfIfCondExpr (getLoc e1))
e2' <- checkE e2 tGoal
e3' <- checkE e3 tGoal
return (EIf e1' e2' e3')
Expand All @@ -423,7 +426,7 @@ checkE expr tGoal =

P.ETyped e t ->
do tSig <- checkTypeOfKind t KType
e' <- checkE e (WithSource tSig TypeFromUserAnnotation)
e' <- checkE e (WithSource tSig TypeFromUserAnnotation (getLoc expr))
checkHasType tSig tGoal
return e'

Expand Down Expand Up @@ -475,13 +478,13 @@ checkRecUpd mb fs tGoal =
P.UpdSet ->
do let src = selSrc s
ft <- newType src KType
v1 <- checkE v (WithSource ft src)
v1 <- checkE v (WithSource ft src (getLoc e))
d <- newHasGoal s (twsType tGoal) ft
pure (hasDoSet d e v1)
P.UpdFun ->
do let src = selSrc s
ft <- newType src KType
v1 <- checkE v (WithSource (tFun ft ft) src)
v1 <- checkE v (WithSource (tFun ft ft) src (getLoc e))
-- XXX: ^ may be used a different src?
d <- newHasGoal s (twsType tGoal) ft
tmp <- newParamName NSValue (packIdent "rf")
Expand All @@ -505,11 +508,11 @@ checkRecUpd mb fs tGoal =


expectSeq :: TypeWithSource -> InferM (Type,Type)
expectSeq tGoal@(WithSource ty src) =
expectSeq tGoal@(WithSource ty src rng) =
case ty of

TUser _ _ ty' ->
expectSeq (WithSource ty' src)
expectSeq (WithSource ty' src rng)

TCon (TC TCSeq) [a,b] ->
return (a,b)
Expand All @@ -521,7 +524,7 @@ expectSeq tGoal@(WithSource ty src) =

_ ->
do tys@(a,b) <- genTys
recordError (TypeMismatch src ty (tSeq a b))
recordErrorLoc rng (TypeMismatch src ty (tSeq a b))
return tys
where
genTys =
Expand All @@ -531,11 +534,11 @@ expectSeq tGoal@(WithSource ty src) =


expectTuple :: Int -> TypeWithSource -> InferM [Type]
expectTuple n tGoal@(WithSource ty src) =
expectTuple n tGoal@(WithSource ty src rng) =
case ty of

TUser _ _ ty' ->
expectTuple n (WithSource ty' src)
expectTuple n (WithSource ty' src rng)

TCon (TC (TCTuple n')) tys | n == n' ->
return tys
Expand All @@ -547,7 +550,7 @@ expectTuple n tGoal@(WithSource ty src) =

_ ->
do tys <- genTys
recordError (TypeMismatch src ty (tTuple tys))
recordErrorLoc rng (TypeMismatch src ty (tTuple tys))
return tys

where
Expand All @@ -558,11 +561,11 @@ expectRec ::
RecordMap Ident (Range, a) ->
TypeWithSource ->
InferM (RecordMap Ident (a, Type))
expectRec fs tGoal@(WithSource ty src) =
expectRec fs tGoal@(WithSource ty src rng) =
case ty of

TUser _ _ ty' ->
expectRec fs (WithSource ty' src)
expectRec fs (WithSource ty' src rng)

TRec ls
| Right r <- zipRecords (\_ (_rng,v) t -> (v,t)) fs ls -> pure r
Expand All @@ -577,24 +580,24 @@ expectRec fs tGoal@(WithSource ty src) =
case ty of
TVar TVFree{} -> do ps <- unify tGoal (TRec tys)
newGoals CtExactType ps
_ -> recordError (TypeMismatch src ty (TRec tys))
_ -> recordErrorLoc rng (TypeMismatch src ty (TRec tys))
return res


expectFin :: Int -> TypeWithSource -> InferM ()
expectFin n tGoal@(WithSource ty src) =
expectFin n tGoal@(WithSource ty src rng) =
case ty of

TUser _ _ ty' ->
expectFin n (WithSource ty' src)
expectFin n (WithSource ty' src rng)

TCon (TC (TCNum n')) [] | toInteger n == n' ->
return ()

_ -> newGoals CtExactType =<< unify tGoal (tNum n)

expectFun :: Maybe Name -> Int -> TypeWithSource -> InferM ([Type],Type)
expectFun mbN n (WithSource ty0 src) = go [] n ty0
expectFun mbN n (WithSource ty0 src rng) = go [] n ty0
where

go tys arity ty
Expand All @@ -612,9 +615,10 @@ expectFun mbN n (WithSource ty0 src) = go [] n ty0
res <- newType TypeOfRes KType
case ty of
TVar TVFree{} ->
do ps <- unify (WithSource ty src) (foldr tFun res args)
do ps <- unify (WithSource ty src rng) (foldr tFun res args)
newGoals CtExactType ps
_ -> recordError (TypeMismatch src ty (foldr tFun res args))
_ -> recordErrorLoc rng
(TypeMismatch src ty (foldr tFun res args))
return (reverse tys ++ args, res)

| otherwise =
Expand All @@ -641,9 +645,11 @@ checkFun (P.FunDesc fun offset) ps e tGoal =
do let descs = [ TypeOfArg (ArgDescr fun (Just n)) | n <- [ 1 + offset .. ] ]

(tys,tRes) <- expectFun fun (length ps) tGoal
largs <- sequence (zipWith checkP ps (zipWith WithSource tys descs))
let srcs = zipWith3 WithSource tys descs (map getLoc ps)
largs <- sequence (zipWith checkP ps srcs)
let ds = Map.fromList [ (thing x, x { thing = t }) | (x,t) <- zip largs tys ]
e1 <- withMonoTypes ds (checkE e (WithSource tRes TypeOfRes))
e1 <- withMonoTypes ds
(checkE e (WithSource tRes TypeOfRes (twsRange tGoal)))

let args = [ (thing x, t) | (x,t) <- zip largs tys ]
return (foldr (\(x,t) b -> EAbs x t b) e1 args)
Expand All @@ -658,11 +664,12 @@ smallest ts = do a <- newType LenOfSeq KNum
return a

checkP :: P.Pattern Name -> TypeWithSource -> InferM (Located Name)
checkP p tGoal@(WithSource _ src) =
checkP p tGoal@(WithSource _ src rng0) =
do (x, t) <- inferP p
ps <- unify tGoal (thing t)
let rng = fromMaybe emptyRange (getLoc p)
let mkErr = recordError . UnsolvedGoals . (:[])
let rngMb = getLoc p `mplus` rng0
rng = fromMaybe emptyRange rngMb
let mkErr = recordErrorLoc rngMb . UnsolvedGoals . (:[])
. Goal (CtPattern src) rng
mapM_ mkErr ps
return (Located (srcRange t) x)
Expand All @@ -679,7 +686,7 @@ inferP pat =

P.PTyped p t ->
do tSig <- checkTypeOfKind t KType
ln <- checkP p (WithSource tSig TypeFromUserAnnotation)
ln <- checkP p (WithSource tSig TypeFromUserAnnotation (getLoc t))
return (thing ln, ln { thing = tSig })

_ -> tcPanic "inferP" [ "Unexpected pattern:", show pat ]
Expand All @@ -691,7 +698,8 @@ inferMatch :: P.Match Name -> InferM (Match, Name, Located Type, Type)
inferMatch (P.Match p e) =
do (x,t) <- inferP p
n <- newType LenOfCompGen KNum
e' <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp)
e' <- checkE e (WithSource (tSeq n (thing t)) GeneratorOfListComp
(getLoc e))
return (From x n (thing t) e', x, t, n)

inferMatch (P.MatchLet b)
Expand Down Expand Up @@ -943,7 +951,7 @@ checkMonoB b t =

P.DExpr e ->
do let nm = thing (P.bName b)
let tGoal = WithSource t (DefinitionOf nm)
let tGoal = WithSource t (DefinitionOf nm) (getLoc b)
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e tGoal
let f = thing (P.bName b)
return Decl { dName = f
Expand Down Expand Up @@ -975,7 +983,7 @@ checkSigB b (Forall as asmps0 t0, validSchema) = case thing (P.bDef b) of
withTParams as $
do (e1,cs0) <- collectGoals $
do let nm = thing (P.bName b)
tGoal = WithSource t0 (DefinitionOf nm)
tGoal = WithSource t0 (DefinitionOf nm) (getLoc b)
e1 <- checkFun (P.FunDesc (Just nm) 0) (P.bParams b) e0 tGoal
addGoals validSchema
() <- simplifyAllConstraints -- XXX: using `asmps` also?
Expand Down
3 changes: 2 additions & 1 deletion src/Cryptol/TypeCheck/Instantiate.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -205,5 +205,6 @@ doInst su' e ps t =
| Set.notMember tp bounds = return []
| otherwise = let a = tpVar tp
src = tvarDesc (tvInfo a)
in unify (WithSource (TVar a) src) ty
rng = Just (tvarSource (tvInfo a))
in unify (WithSource (TVar a) src rng) ty

21 changes: 15 additions & 6 deletions src/Cryptol/TypeCheck/Monad.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -331,12 +331,21 @@ curRange = IM $ asks iRange

-- | Report an error.
recordError :: Error -> InferM ()
recordError e =
do r <- case e of
AmbiguousSize d _ -> return (tvarSource d)
_ -> curRange
recordError = recordErrorLoc Nothing

-- | Report an error.
recordErrorLoc :: Maybe Range -> Error -> InferM ()
recordErrorLoc rng e =
do r <- case rng of
Just r -> pure r
Nothing -> case e of
AmbiguousSize d _ -> return (tvarSource d)
_ -> curRange
IM $ sets_ $ \s -> s { iErrors = (r,e) : iErrors s }




recordWarning :: Warning -> InferM ()
recordWarning w =
unless ignore $
Expand Down Expand Up @@ -549,7 +558,7 @@ newType src k = TVar `fmap` newTVar src k

-- | Record that the two types should be syntactically equal.
unify :: TypeWithSource -> Type -> InferM [Prop]
unify (WithSource t1 src) t2 =
unify (WithSource t1 src rng) t2 =
do t1' <- applySubst t1
t2' <- applySubst t2
let ((su1, ps), errs) = runResult (mgu t1' t2')
Expand All @@ -565,7 +574,7 @@ unify (WithSource t1 src) t2 =
UniNonPoly x t -> NotForAll src x t
case errs of
[] -> return ps
_ -> do mapM_ (recordError . toError) errs
_ -> do mapM_ (recordErrorLoc rng . toError) errs
return []

-- | Apply the accumulated substitution to something with free type variables.
Expand Down
13 changes: 8 additions & 5 deletions src/Cryptol/TypeCheck/Solver/Selector.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -8,6 +8,7 @@
{-# LANGUAGE PatternGuards, Safe #-}
module Cryptol.TypeCheck.Solver.Selector (tryHasGoal) where

import Cryptol.Parser.Position(Range)
import Cryptol.TypeCheck.AST
import Cryptol.TypeCheck.InferTypes
import Cryptol.TypeCheck.Monad( InferM, unify, newGoals
Expand Down Expand Up @@ -41,16 +42,16 @@ listType n =
return (tSeq (tNum n) elems)


improveSelector :: Selector -> Type -> InferM Bool
improveSelector sel outerT =
improveSelector :: Maybe Range -> Selector -> Type -> InferM Bool
improveSelector rng sel outerT =
case sel of
RecordSel _ mb -> cvt recordType mb
TupleSel _ mb -> cvt tupleType mb
ListSel _ mb -> cvt listType mb
where
cvt _ Nothing = return False
cvt f (Just a) = do ty <- f a
ps <- unify (WithSource outerT (selSrc sel)) ty
ps <- unify (WithSource outerT (selSrc sel) rng) ty
newGoals CtExactType ps
newT <- applySubst outerT
return (newT /= outerT)
Expand Down Expand Up @@ -117,13 +118,15 @@ solveSelector sel outerT =
tryHasGoal :: HasGoal -> InferM (Bool, Bool) -- ^ changes, solved
tryHasGoal has
| TCon (PC (PHas sel)) [ th, ft ] <- goal (hasGoal has) =
do imped <- improveSelector sel th
do let rng = Just (goalRange (hasGoal has))
imped <- improveSelector rng sel th
outerT <- tNoUser `fmap` applySubst th
mbInnerT <- solveSelector sel outerT
case mbInnerT of
Nothing -> return (imped, False)
Just innerT ->
do newGoals CtExactType =<< unify (WithSource innerT (selSrc sel)) ft
do newGoals CtExactType =<<
unify (WithSource innerT (selSrc sel) rng) ft
oT <- applySubst outerT
iT <- applySubst innerT
sln <- mkSelSln sel oT iT
Expand Down
1 change: 1 addition & 0 deletions src/Cryptol/TypeCheck/Type.hs
View file
Original file line number Diff line number Diff line change
Expand Up @@ -231,6 +231,7 @@ tvSourceName tvs =
data TypeWithSource = WithSource
{ twsType :: Type
, twsSource :: TypeSource
, twsRange :: !(Maybe Range)
}


Expand Down
Loading

0 comments on commit 851ef89

Please sign in to comment.