diff --git a/idris.cabal b/idris.cabal index 4112184a4..09039ccc4 100644 --- a/idris.cabal +++ b/idris.cabal @@ -1,5 +1,5 @@ Name: idris -Version: 0.9.9.3 +Version: 0.9.9.4 License: BSD3 License-file: LICENSE Author: Edwin Brady diff --git a/src/Core/Constraints.hs b/src/Core/Constraints.hs index 03d8f4634..254ed4f11 100644 --- a/src/Core/Constraints.hs +++ b/src/Core/Constraints.hs @@ -38,7 +38,7 @@ mkRels ((c, f) : cs) acc acyclic :: Relations -> [UExp] -> TC () -acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs +acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs where checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC () checkCycle fc r path inc [] = return () diff --git a/src/Core/Evaluate.hs b/src/Core/Evaluate.hs index 1fd5b2024..217f22ce4 100644 --- a/src/Core/Evaluate.hs +++ b/src/Core/Evaluate.hs @@ -700,10 +700,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict) access = case lookupDefAcc n False uctxt of [(_, acc)] -> acc _ -> Public - ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot, - simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct, - simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl, - simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of + ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot, + simpleCase tcase covering reflect CompileTime emptyFC ps_ct, + simpleCase tcase covering reflect CompileTime emptyFC ps_inl, + simpleCase tcase covering reflect RunTime emptyFC ps_rt) of (OK (CaseDef args_tot sc_tot _), OK (CaseDef args_ct sc_ct _), OK (CaseDef args_inl sc_inl _), @@ -730,7 +730,7 @@ simplifyCasedef n uctxt [(CaseOp ci ty ps_in ps cd, acc, tot)] -> let ps_in' = map simpl ps_in pdef = map debind ps_in' in - case simpleCase False True False CompileTime (FC "" 0) pdef of + case simpleCase False True False CompileTime emptyFC pdef of OK (CaseDef args sc _) -> addDef n (CaseOp ci ty ps_in' ps (cd { cases_totcheck = (args, sc) }), diff --git a/src/Core/TT.hs b/src/Core/TT.hs index db66c29dc..34b7a9fa7 100644 --- a/src/Core/TT.hs +++ b/src/Core/TT.hs @@ -38,20 +38,29 @@ data Option = TTypeInTType | CheckConv deriving Eq --- | Source location. These are typically produced by the parser 'Idris.Parser.pfc' +-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC' data FC = FC { fc_fname :: String, -- ^ Filename - fc_line :: Int -- ^ Line number - } - deriving Eq + fc_line :: Int, -- ^ Line number + fc_column :: Int -- ^ Column number + } deriving Eq + +-- | Empty source location +emptyFC :: FC +emptyFC = fileFC "" + +-- | Source location with file only +fileFC :: String -> FC +fileFC s = FC s 0 0 + {-! deriving instance Binary FC !-} instance Sized FC where - size (FC f l) = 1 + length f + size (FC f l c) = 1 + length f instance Show FC where - show (FC f l) = f ++ ":" ++ show l + show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c data Err = Msg String | InternalMsg String diff --git a/src/Idris/AbsSyntax.hs b/src/Idris/AbsSyntax.hs index 92a1d9dd5..f872a74fa 100644 --- a/src/Idris/AbsSyntax.hs +++ b/src/Idris/AbsSyntax.hs @@ -314,7 +314,10 @@ iputStrLn s = do i <- getIState (fn, ':':rest) -> case span isDigit rest of ([], ':':msg) -> write ([], msg) -> write - (num, ':':msg) -> iWarn (FC fn (read num)) msg + (row, ':':rest') -> + case span isDigit rest' of + ([], msg) -> iWarn (FC fn (read row) 0) msg + (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg _ -> write where write = runIO . putStrLn $ convSExp "write-string" s n @@ -576,7 +579,7 @@ setTypeCase t = do i <- getIState -- For inferring types of things -bi = FC "builtin" 0 +bi = fileFC "builtin" inferTy = MN 0 "__Infer" inferCon = MN 0 "__infer" @@ -1417,8 +1420,8 @@ substMatchShadow n shs tm t = sm shs t where sm xs (PPi p x t sc) | x `elem` xs = let x' = nextName x in - PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t)) - (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc)) + PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t)) + (sm (x':xs) (substMatch x (PRef emptyFC x') sc)) | otherwise = PPi p x (sm xs t) (sm (x : xs) sc) sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as) sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as) diff --git a/src/Idris/AbsSyntaxTree.hs b/src/Idris/AbsSyntaxTree.hs index 924079e37..b8a0f91d6 100644 --- a/src/Idris/AbsSyntaxTree.hs +++ b/src/Idris/AbsSyntaxTree.hs @@ -561,7 +561,7 @@ data PTerm = PQuote Raw | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice | PUnifyLog PTerm -- ^ dump a trace of unifications when building term | PNoImplicits PTerm -- ^ never run implicit converions on the term - deriving Eq + deriving (Eq, Show) {-! deriving instance Binary PTerm !-} @@ -642,7 +642,7 @@ data PDo' t = DoExp FC t | DoBindP FC t t | DoLet FC Name t t | DoLetP FC t t - deriving (Eq, Functor) + deriving (Eq, Functor, Show) {-! deriving instance Binary PDo' !-} @@ -774,7 +774,7 @@ initDSL = DSL (PRef f (UN ">>=")) Nothing Nothing Nothing - where f = FC "(builtin)" 0 + where f = fileFC "(builtin)" data Using = UImplicit Name PTerm | UConstraint Name [Name] @@ -807,8 +807,8 @@ expandNS syn n = case syn_namespace syn of --- Pretty printing declarations and terms -instance Show PTerm where - show tm = showImp Nothing False False tm +{-instance Show PTerm where-} + {-show tm = showImp Nothing False False tm-} instance Pretty PTerm where pretty = prettyImp False diff --git a/src/Idris/DSL.hs b/src/Idris/DSL.hs index 7e2949b54..71a80de8b 100644 --- a/src/Idris/DSL.hs +++ b/src/Idris/DSL.hs @@ -22,12 +22,12 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in expandDo :: DSL -> PTerm -> PTerm expandDo dsl (PLam n ty tm) | Just lam <- dsl_lambda dsl - = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in + = let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in expandDo dsl sc expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm) expandDo dsl (PLet n ty v tm) | Just letb <- dsl_let dsl - = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in + = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in expandDo dsl sc expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm) expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm) diff --git a/src/Idris/Delaborate.hs b/src/Idris/Delaborate.hs index 93de83cc3..fa8bc797e 100644 --- a/src/Idris/Delaborate.hs +++ b/src/Idris/Delaborate.hs @@ -30,7 +30,7 @@ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any -> Term -> Bool -> PTerm delabTy' ist imps tm fullname = de [] imps tm where - un = FC "(val)" 0 + un = fileFC "(val)" de env _ (App f a) = deFn env f [a] de env _ (V i) | i < length env = PRef un (snd (env!!i)) diff --git a/src/Idris/ElabDecls.hs b/src/Idris/ElabDecls.hs index 821bdfe80..efe9b02b9 100644 --- a/src/Idris/ElabDecls.hs +++ b/src/Idris/ElabDecls.hs @@ -220,7 +220,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons) elabPrims :: Idris () elabPrims = do mapM_ (elabDecl EAll toplevel) - (map (PData "" defaultSyntax (FC "builtin" 0) False) + (map (PData "" defaultSyntax (fileFC "builtin") False) [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]) mapM_ elabPrim primitives -- Special case prim__believe_me because it doesn't work on just constants @@ -746,15 +746,15 @@ elabVal info aspat tm_in -- (build i info aspat (MN 0 "val") tm)) tclift (elaborate ctxt (MN 0 "val") infP [] (build i info aspat (MN 0 "val") (infTerm tm))) - def' <- checkDef (FC "(input)" 0) defer + def' <- checkDef (fileFC "(input)") defer addDeferred def' mapM_ (elabCaseBlock info []) is logLvl 3 ("Value: " ++ show tm') - recheckC (FC "(input)" 0) [] tm' + recheckC (fileFC "(input)") [] tm' let vtm = getInferTerm tm' logLvl 2 (show vtm) - recheckC (FC "(input)" 0) [] vtm + recheckC (fileFC "(input)") [] vtm -- checks if the clause is a possible left hand side. Returns the term if -- possible, otherwise Nothing. @@ -1051,7 +1051,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock) logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++ showImp Nothing True False toplhs) case matchClause i toplhs tm of - Left f -> ifail $ show fc ++ ":with clause does not match top level" + Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level") Right mvars -> do logLvl 3 ("Match vars : " ++ show mvars) lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w @@ -1063,7 +1063,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock) showImp Nothing True False toplhs) withs' <- mapM (mkAuxC wname toplhs ns ns') withs case matchClause i toplhs tm of - Left _ -> ifail $ show fc ++ "with clause does not match top level" + Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level") Right mvars -> do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w return $ PWith fc wname lhs ws wval withs' @@ -1190,7 +1190,7 @@ elabClass info syn doc fc constraints tn ps ds let mnames = take (length all) $ map (\x -> MN x "meth") [0..] let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames) let lhs = PApp fc (PRef fc cfn) [pconst capp] - let rhs = PResolveTC (FC "HACK" 0) + let rhs = PResolveTC (fileFC "HACK") let ty = PPi constraint (MN 0 "pc") c con iLOG (showImp Nothing True False ty) iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs) diff --git a/src/Idris/ElabTerm.hs b/src/Idris/ElabTerm.hs index 68a426267..e5329847f 100644 --- a/src/Idris/ElabTerm.hs +++ b/src/Idris/ElabTerm.hs @@ -149,7 +149,7 @@ elab ist info pattern tcgen fn tm elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon)) (elab' ina (PRef fc unitTy)) elab' ina (PFalse fc) = elab' ina (PRef fc falseTy) - elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes + elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes = resolveTC 5 fn ist elab' ina (PResolveTC fc) | True = do c <- unique_hole (MN 0 "class") @@ -548,7 +548,7 @@ elab ist info pattern tcgen fn tm PAlternative True (map (mkCoerce t) cs)] return t' where - mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears! + mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears! addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)]) elabArgs ina failed fc retry [] _ @@ -633,7 +633,7 @@ pruneByType t _ as = as trivial :: IState -> ElabD () trivial ist = try' (do elab ist toplevel False False (MN 0 "tac") - (PRefl (FC "prf" 0) Placeholder) + (PRefl (fileFC "prf") Placeholder) return ()) (do env <- get_env g <- goal @@ -647,7 +647,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac") g <- goal if all (\n -> not (n `elem` hs)) (freeNames (binderTy b)) then try' (elab ist toplevel False False - (MN 0 "tac") (PRef (FC "prf" 0) x)) + (MN 0 "tac") (PRef (fileFC "prf") x)) (tryAll xs) True else tryAll xs diff --git a/src/Idris/Error.hs b/src/Idris/Error.hs index 7c3f905e8..0cbb484d0 100644 --- a/src/Idris/Error.hs +++ b/src/Idris/Error.hs @@ -50,7 +50,7 @@ ierror = throwError tclift :: TC a -> Idris a tclift (OK v) = return v -tclift (Error err@(At (FC f l) e)) = do setErrLine l ; throwError err +tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err tclift (Error err) = throwError err tctry :: TC a -> TC a -> Idris a @@ -60,7 +60,9 @@ tctry tc1 tc2 Error err -> tclift tc2 getErrLine :: Err -> Int -getErrLine (At (FC _ l) _) = l +getErrLine (At (FC _ l _) _) = l getErrLine _ = 0 - +getErrColumn :: Err -> Int +getErrColumn (At (FC _ _ c) _) = c +getErrColumn _ = 0 diff --git a/src/Idris/IBC.hs b/src/Idris/IBC.hs index fcff6000f..80ed46ee1 100644 --- a/src/Idris/IBC.hs +++ b/src/Idris/IBC.hs @@ -346,13 +346,15 @@ instance Binary CGInfo where return (CGInfo x1 x2 x3 x4 x5) instance Binary FC where - put (FC x1 x2) + put (FC x1 x2 x3) = do put x1 put x2 + put x3 get = do x1 <- get x2 <- get - return (FC x1 x2) + x3 <- get + return (FC x1 x2 x3) instance Binary Name where diff --git a/src/Idris/ParseHelpers.hs b/src/Idris/ParseHelpers.hs index cd432aa56..1cdfea2c2 100644 --- a/src/Idris/ParseHelpers.hs +++ b/src/Idris/ParseHelpers.hs @@ -254,13 +254,19 @@ fileName _ = "(interactive)" lineNum :: Delta -> Int lineNum (Lines l _ _ _) = fromIntegral l + 1 lineNum (Directed _ l _ _ _) = fromIntegral l + 1 +lineNum _ = 0 + +{- | Get column number from position -} +columnNum :: Delta -> Int +columnNum pos = fromIntegral (column pos) + 1 + {- | Get file position as FC -} getFC :: MonadicParsing m => m FC getFC = do s <- position let (dir, file) = splitFileName (fileName s) let f = if dir == addTrailingPathSeparator "." then file else fileName s - return $ FC f (lineNum s) + return $ FC f (lineNum s) (columnNum s) {-* Syntax helpers-} -- | Bind constraints to term diff --git a/src/Idris/Parser.hs b/src/Idris/Parser.hs index aab57479d..2ede63f22 100644 --- a/src/Idris/Parser.hs +++ b/src/Idris/Parser.hs @@ -1032,7 +1032,7 @@ loadSource lidr f toMutual :: PDecl -> PDecl toMutual m@(PMutual _ d) = m toMutual (PNamespace x ds) = PNamespace x (map toMutual ds) - toMutual x = let r = PMutual (FC "single mutual" 0) [x] in + toMutual x = let r = PMutual (fileFC "single mutual") [x] in case x of PClauses _ _ _ _ -> r PClass _ _ _ _ _ _ _ -> r diff --git a/src/Idris/Prover.hs b/src/Idris/Prover.hs index a6cb7221c..1ab325e8a 100644 --- a/src/Idris/Prover.hs +++ b/src/Idris/Prover.hs @@ -65,9 +65,9 @@ prove ctxt lit n ty ideslavePutSExp "end-proof-mode" n let proofs = proof_list i putIState (i { proof_list = (n, prf) : proofs }) - let tree = simpleCase False True False CompileTime (FC "proof" 0) [([], P Ref n ty, tm)] + let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)] logLvl 3 (show tree) - (ptm, pty) <- recheckC (FC "proof" 0) [] tm + (ptm, pty) <- recheckC (fileFC "proof") [] tm logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++ "Expected type:" ++ show ty) case converts ctxt [] ty pty of diff --git a/src/Idris/REPL.hs b/src/Idris/REPL.hs index 447410559..76433b377 100644 --- a/src/Idris/REPL.hs +++ b/src/Idris/REPL.hs @@ -491,7 +491,7 @@ process fn (Prove n') prover (lit fn) n -- recheck totality i <- getIState - totcheck (FC "(input)" 0, n) + totcheck (fileFC "(input)", n) mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i) mapM_ checkDeclTotality (idris_totcheck i) @@ -522,13 +522,13 @@ process fn Execute = do (m, _) <- elabVal toplevel False compile t tmpn m runIO $ system tmpn return () - where fc = FC "main" 0 + where fc = fileFC "main" process fn (Compile codegen f) = do (m, _) <- elabVal toplevel False (PApp fc (PRef fc (UN "run__IO")) [pexp $ PRef fc (NS (UN "main") ["Main"])]) compile codegen f m - where fc = FC "main" 0 + where fc = fileFC "main" process fn (LogLvl i) = setLogLevel i -- Elaborate as if LHS of a pattern (debug command) process fn (Pattelab t) diff --git a/src/Idris/Unlit.hs b/src/Idris/Unlit.hs index 1b4bd1922..aa6aef49b 100644 --- a/src/Idris/Unlit.hs +++ b/src/Idris/Unlit.hs @@ -24,8 +24,8 @@ check f l [x] = return () check f l [] = return () chkAdj :: FilePath -> Int -> LineType -> LineType -> TC () -chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment -chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment +chkAdj f l Prog Comm = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column? +chkAdj f l Comm Prog = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column? chkAdj f l _ _ = return () diff --git a/test/reg003/expected b/test/reg003/expected index 33bd95708..ab6e1890c 100644 --- a/test/reg003/expected +++ b/test/reg003/expected @@ -1,7 +1,7 @@ -reg003a.idr:4:When elaborating constructor ECons: +reg003a.idr:4:20:When elaborating constructor ECons: No such variable OddList -reg003a.idr:7:When elaborating constructor OCons: +reg003a.idr:7:20:When elaborating constructor OCons: No such variable EvenList -reg003a.idr:9:When elaborating type of test: +reg003a.idr:9:8:When elaborating type of test: No such variable EvenList -reg003a.idr:10:No type declaration for test +reg003a.idr:10:1:No type declaration for test diff --git a/test/reg006/expected b/test/reg006/expected index 14948de07..adc46c9a6 100644 --- a/test/reg006/expected +++ b/test/reg006/expected @@ -1 +1 @@ -reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.case block in lookup +reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup diff --git a/test/reg007/expected b/test/reg007/expected index 321f17baa..7d7c0b19f 100644 --- a/test/reg007/expected +++ b/test/reg007/expected @@ -1,5 +1,5 @@ -reg007.lidr:8:A.n is already defined -reg007.lidr:12:When elaborating right hand side of hurrah: +reg007.lidr:8:1:A.n is already defined +reg007.lidr:12:9:When elaborating right hand side of hurrah: Can't unify n = A.lala with diff --git a/test/reg010/expected b/test/reg010/expected index 439cbdef7..598b8c5f5 100644 --- a/test/reg010/expected +++ b/test/reg010/expected @@ -1,4 +1,4 @@ -reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst: +reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst: Can't unify P x with diff --git a/test/reg018/expected b/test/reg018/expected index b0f79938c..97f416996 100644 --- a/test/reg018/expected +++ b/test/reg018/expected @@ -1,4 +1,4 @@ -reg018a.idr:16:conat.minusCoNat is not productive -reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB -reg018c.idr:19:CodataTest.inf is not productive -reg018d.idr:5:Main.pull is not total as there are missing cases +reg018a.idr:16:1:conat.minusCoNat is not productive +reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB +reg018c.idr:19:1:CodataTest.inf is not productive +reg018d.idr:5:1:Main.pull is not total as there are missing cases diff --git a/test/reg023/expected b/test/reg023/expected index b2ad87203..22d772f25 100644 --- a/test/reg023/expected +++ b/test/reg023/expected @@ -1,4 +1,4 @@ -reg023.idr:7:When elaborating right hand side of bad: +reg023.idr:7:5:When elaborating right hand side of bad: Can't unify Nat with diff --git a/test/test003/expected b/test/test003/expected index cf72b3c24..6d00f4529 100644 --- a/test/test003/expected +++ b/test/test003/expected @@ -1,4 +1,4 @@ -./test003a.lidr:1:Program line next to comment +./test003a.lidr:1:0:Program line next to comment a d zabcdefg diff --git a/test/test010/expected b/test/test010/expected index fc3607db2..25e1ed479 100644 --- a/test/test010/expected +++ b/test/test010/expected @@ -1,3 +1,3 @@ -test010.idr:13:foo is possibly not total due to: MkBad -test010a.idr:9:main.bar is possibly not total due to: main.MkBad -test010b.idr:9:main.bar is possibly not total due to: main.MkBad +test010.idr:13:1:foo is possibly not total due to: MkBad +test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad +test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad diff --git a/test/test012/expected b/test/test012/expected index 7099b10f5..91c359446 100644 --- a/test/test012/expected +++ b/test/test012/expected @@ -1 +1 @@ -test012a.idr:7:x is not an accessible pattern variable +test012a.idr:7:1:x is not an accessible pattern variable diff --git a/test/test017/expected b/test/test017/expected index da0f2a627..a96bb31ae 100644 --- a/test/test017/expected +++ b/test/test017/expected @@ -1,2 +1,2 @@ -test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans -test017b.idr:4:foo.foo is possibly not total due to recursive path foo.foo +test017a.idr:5:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans +test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo diff --git a/test/test020/expected b/test/test020/expected index e9cda9b0e..c8ab0d6db 100644 --- a/test/test020/expected +++ b/test/test020/expected @@ -1,5 +1,5 @@ When elaborating right hand side of foo: -test020a.idr:14:Can't unify +test020a.idr:14:18:Can't unify Vect n a with List a diff --git a/test/test030/expected b/test/test030/expected index 6f5eba975..a6cc166c5 100644 --- a/test/test030/expected +++ b/test/test030/expected @@ -1,4 +1,4 @@ -test030a.idr:12:When elaborating right hand side of testReflect1: +test030a.idr:12:14:When elaborating right hand side of testReflect1: Can't unify IsJust (Just x) with