bc0ebee · Idris-dev · git.iko.soy

src/Core/Constraints.hs+1−1

compare with master

unifiedsplit

@@ -38,7 +38,7 @@ mkRels ((c, f) : cs) acc

38

39

40acyclic :: Relations -> [UExp] -> TC ()

41−acyclic r cvs = checkCycle (FC "root" 0) r [] 0 cvs

41+acyclic r cvs = checkCycle (fileFC "root") r [] 0 cvs

42 where

43 checkCycle :: FC -> Relations -> [(UExp, FC)] -> Int -> [UExp] -> TC ()

44 checkCycle fc r path inc [] = return ()

src/Core/Evaluate.hs+5−5

@@ -700,10 +700,10 @@ addCasedef n ci@(CaseInfo alwaysInline tcdict)

700 access = case lookupDefAcc n False uctxt of

701 [(_, acc)] -> acc

702 _ -> Public

703− ctxt' = case (simpleCase tcase covering reflect CompileTime (FC "" 0) ps_tot,

703+ ctxt' = case (simpleCase tcase covering reflect CompileTime emptyFC ps_tot,

704− simpleCase tcase covering reflect CompileTime (FC "" 0) ps_ct,

704+ simpleCase tcase covering reflect CompileTime emptyFC ps_ct,

705− simpleCase tcase covering reflect CompileTime (FC "" 0) ps_inl,

705+ simpleCase tcase covering reflect CompileTime emptyFC ps_inl,

706− simpleCase tcase covering reflect RunTime (FC "" 0) ps_rt) of

706+ simpleCase tcase covering reflect RunTime emptyFC ps_rt) of

707 (OK (CaseDef args_tot sc_tot _),

708 OK (CaseDef args_ct sc_ct _),

709 OK (CaseDef args_inl sc_inl _),

@@ -730,7 +730,7 @@ simplifyCasedef n uctxt

730 [(CaseOp ci ty ps_in ps cd, acc, tot)] ->

731 let ps_in' = map simpl ps_in

732 pdef = map debind ps_in' in

733− case simpleCase False True False CompileTime (FC "" 0) pdef of

733+ case simpleCase False True False CompileTime emptyFC pdef of

734 OK (CaseDef args sc _) ->

735 addDef n (CaseOp ci

736 ty ps_in' ps (cd { cases_totcheck = (args, sc) }),

src/Core/TT.hs+25−5

@@ -38,20 +38,40 @@ data Option = TTypeInTType

38 | CheckConv

39 deriving Eq

40

41−-- | Source location. These are typically produced by the parser 'Idris.Parser.pfc'

41+-- | Source location. These are typically produced by the parser 'Idris.Parser.getFC'

42data FC = FC { fc_fname :: String, -- ^ Filename

43− fc_line :: Int -- ^ Line number

43+ fc_line :: Int, -- ^ Line number

44+ fc_column :: Int -- ^ Column number

44 }

45 }

45− deriving Eq

46+

47+-- | Ignore source location equality (so deriving classes do not compare FCs)

48+instance Eq FC where

49+ _ == _ = True

50+

51+-- | FC with equality

52+newtype FC' = FC' { unwrapFC :: FC }

53+

54+instance Eq FC' where

55+ FC' fc == FC' fc' = fcEq fc fc'

56+ where fcEq (FC n l c) (FC n' l' c') = n == n' && l == l' && c == c'

57+

58+-- | Empty source location

59+emptyFC :: FC

60+emptyFC = fileFC ""

61+

62+-- | Source location with file only

63+fileFC :: String -> FC

64+fileFC s = FC s 0 0

65+

46{-!

66{-!

47deriving instance Binary FC

67deriving instance Binary FC

48!-}

68!-}

49

69

50instance Sized FC where

70instance Sized FC where

51− size (FC f l) = 1 + length f

71+ size (FC f l c) = 1 + length f

52

72

53instance Show FC where

73instance Show FC where

54− show (FC f l) = f ++ ":" ++ show l

74+ show (FC f l c) = f ++ ":" ++ show l ++ ":" ++ show c

55

75

56data Err = Msg String

76data Err = Msg String

57 | InternalMsg String

77 | InternalMsg String

src/Idris/AbsSyntax.hs+7−4

@@ -314,7 +314,10 @@ iputStrLn s = do i <- getIState

314 (fn, ':':rest) -> case span isDigit rest of

315 ([], ':':msg) -> write

316 ([], msg) -> write

317+ (row, ':':rest') ->

318+ case span isDigit rest' of

319+ ([], msg) -> iWarn (FC fn (read row) 0) msg

317− (num, ':':msg) -> iWarn (FC fn (read num)) msg

320+ (col, ':':msg) -> iWarn (FC fn (read row) (read col)) msg

318 _ -> write

321 _ -> write

319 where write = runIO . putStrLn $ convSExp "write-string" s n

322 where write = runIO . putStrLn $ convSExp "write-string" s n

320

323

@@ -576,7 +579,7 @@ setTypeCase t = do i <- getIState

576

579

577-- For inferring types of things

580-- For inferring types of things

578

581

579−bi = FC "builtin" 0

582+bi = fileFC "builtin"

580

583

581inferTy = MN 0 "__Infer"

584inferTy = MN 0 "__Infer"

582inferCon = MN 0 "__infer"

585inferCon = MN 0 "__infer"

@@ -1420,8 +1423,8 @@ substMatchShadow n shs tm t = sm shs t where

1420 sm xs (PPi p x t sc)

1423 sm xs (PPi p x t sc)

1421 | x `elem` xs

1424 | x `elem` xs

1422 = let x' = nextName x in

1425 = let x' = nextName x in

1423− PPi p x' (sm (x':xs) (substMatch x (PRef (FC "" 0) x') t))

1426+ PPi p x' (sm (x':xs) (substMatch x (PRef emptyFC x') t))

1424− (sm (x':xs) (substMatch x (PRef (FC "" 0) x') sc))

1427+ (sm (x':xs) (substMatch x (PRef emptyFC x') sc))

1425 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1428 | otherwise = PPi p x (sm xs t) (sm (x : xs) sc)

1426 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1429 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

1427 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

1430 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

src/Idris/AbsSyntaxTree.hs+4−2

@@ -561,7 +561,9 @@ data PTerm = PQuote Raw

561 | PCoerced PTerm -- ^ To mark a coerced argument, so as not to coerce twice

562 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

563 | PNoImplicits PTerm -- ^ never run implicit converions on the term

564− deriving Eq

564+ deriving Eq

565+

566+

565{-!

567{-!

566deriving instance Binary PTerm

568deriving instance Binary PTerm

567!-}

569!-}

@@ -774,7 +776,7 @@ initDSL = DSL (PRef f (UN ">>="))

774 Nothing

776 Nothing

775 Nothing

777 Nothing

776 Nothing

778 Nothing

777− where f = FC "(builtin)" 0

779+ where f = fileFC "(builtin)"

778

780

779data Using = UImplicit Name PTerm

781data Using = UImplicit Name PTerm

780 | UConstraint Name [Name]

782 | UConstraint Name [Name]

src/Idris/DSL.hs+2−2

@@ -22,12 +22,12 @@ desugar syn i t = let t' = expandDo (dsl_info syn) t in

22expandDo :: DSL -> PTerm -> PTerm

23expandDo dsl (PLam n ty tm)

24 | Just lam <- dsl_lambda dsl

25− = let sc = PApp (FC "(dsl)" 0) lam [pexp (var dsl n tm 0)] in

25+ = let sc = PApp (fileFC "(dsl)") lam [pexp (var dsl n tm 0)] in

26 expandDo dsl sc

27expandDo dsl (PLam n ty tm) = PLam n (expandDo dsl ty) (expandDo dsl tm)

28expandDo dsl (PLet n ty v tm)

29 | Just letb <- dsl_let dsl

30− = let sc = PApp (FC "(dsl)" 0) letb [pexp v, pexp (var dsl n tm 0)] in

30+ = let sc = PApp (fileFC "(dsl)") letb [pexp v, pexp (var dsl n tm 0)] in

31 expandDo dsl sc

32expandDo dsl (PLet n ty v tm) = PLet n (expandDo dsl ty) (expandDo dsl v) (expandDo dsl tm)

33expandDo dsl (PPi p n ty tm) = PPi p n (expandDo dsl ty) (expandDo dsl tm)

src/Idris/Delaborate.hs+1−1

@@ -30,7 +30,7 @@ delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

30 -> Term -> Bool -> PTerm

31delabTy' ist imps tm fullname = de [] imps tm

32 where

33− un = FC "(val)" 0

33+ un = fileFC "(val)"

34

35 de env _ (App f a) = deFn env f [a]

36 de env _ (V i) | i < length env = PRef un (snd (env!!i))

src/Idris/ElabDecls.hs+7−7

@@ -220,7 +220,7 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)

220

221elabPrims :: Idris ()

222elabPrims = do mapM_ (elabDecl EAll toplevel)

223− (map (PData "" defaultSyntax (FC "builtin" 0) False)

223+ (map (PData "" defaultSyntax (fileFC "builtin") False)

224 [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])

225 mapM_ elabPrim primitives

226 -- Special case prim__believe_me because it doesn't work on just constants

@@ -746,15 +746,15 @@ elabVal info aspat tm_in

746-- (build i info aspat (MN 0 "val") tm))

747 tclift (elaborate ctxt (MN 0 "val") infP []

748 (build i info aspat (MN 0 "val") (infTerm tm)))

749− def' <- checkDef (FC "(input)" 0) defer

749+ def' <- checkDef (fileFC "(input)") defer

750 addDeferred def'

751 mapM_ (elabCaseBlock info []) is

752

753 logLvl 3 ("Value: " ++ show tm')

754− recheckC (FC "(input)" 0) [] tm'

754+ recheckC (fileFC "(input)") [] tm'

755 let vtm = getInferTerm tm'

756 logLvl 2 (show vtm)

757− recheckC (FC "(input)" 0) [] vtm

757+ recheckC (fileFC "(input)") [] vtm

758

759-- checks if the clause is a possible left hand side. Returns the term if

760-- possible, otherwise Nothing.

@@ -1051,7 +1051,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1051 logLvl 2 ("Matching " ++ showImp Nothing True False tm ++ " against " ++

1052 showImp Nothing True False toplhs)

1053 case matchClause i toplhs tm of

1054− Left f -> ifail $ show fc ++ ":with clause does not match top level"

1054+ Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ ":with clause does not match top level")

1055 Right mvars ->

1056 do logLvl 3 ("Match vars : " ++ show mvars)

1057 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)

1063 showImp Nothing True False toplhs)

1064 withs' <- mapM (mkAuxC wname toplhs ns ns') withs

1065 case matchClause i toplhs tm of

1066− Left _ -> ifail $ show fc ++ "with clause does not match top level"

1066+ Left (a,b) -> trace ("matchClause: " ++ show a ++ " =/= " ++ show b) (ifail $ show fc ++ "with clause does not match top level")

1067 Right mvars ->

1068 do lhs <- updateLHS n wname mvars ns ns' (fullApp tm) w

1069 return $ PWith fc wname lhs ws wval withs'

@@ -1190,7 +1190,7 @@ elabClass info syn doc fc constraints tn ps ds

1190 let mnames = take (length all) $ map (\x -> MN x "meth") [0..]

1191 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

1192 let lhs = PApp fc (PRef fc cfn) [pconst capp]

1193− let rhs = PResolveTC (FC "HACK" 0)

1193+ let rhs = PResolveTC (fileFC "HACK")

1194 let ty = PPi constraint (MN 0 "pc") c con

1195 iLOG (showImp Nothing True False ty)

1196 iLOG (showImp Nothing True False lhs ++ " = " ++ showImp Nothing True False rhs)

src/Idris/ElabTerm.hs+4−4

@@ -149,7 +149,7 @@ elab ist info pattern tcgen fn tm

149 elab' ina (PTrue fc) = try (elab' ina (PRef fc unitCon))

150 (elab' ina (PRef fc unitTy))

151 elab' ina (PFalse fc) = elab' ina (PRef fc falseTy)

152− elab' ina (PResolveTC (FC "HACK" _)) -- for chasing parent classes

152+ elab' ina (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

153 = resolveTC 5 fn ist

154 elab' ina (PResolveTC fc)

155 | True = do c <- unique_hole (MN 0 "class")

@@ -548,7 +548,7 @@ elab ist info pattern tcgen fn tm

548 PAlternative True (map (mkCoerce t) cs)]

549 return t'

550 where

551− mkCoerce t n = let fc = FC "Coercion" 0 in -- line never appears!

551+ mkCoerce t n = let fc = fileFC "Coercion" in -- line never appears!

552 addImpl ist (PApp fc (PRef fc n) [pexp (PCoerced t)])

553

554 elabArgs ina failed fc retry [] _

@@ -633,7 +633,7 @@ pruneByType t _ as = as

633

634trivial :: IState -> ElabD ()

635trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

636− (PRefl (FC "prf" 0) Placeholder)

636+ (PRefl (fileFC "prf") Placeholder)

637 return ())

638 (do env <- get_env

639 g <- goal

@@ -647,7 +647,7 @@ trivial ist = try' (do elab ist toplevel False False (MN 0 "tac")

647 g <- goal

648 if all (\n -> not (n `elem` hs)) (freeNames (binderTy b))

649 then try' (elab ist toplevel False False

650− (MN 0 "tac") (PRef (FC "prf" 0) x))

650+ (MN 0 "tac") (PRef (fileFC "prf") x))

651 (tryAll xs) True

652 else tryAll xs

653

src/Idris/Error.hs+5−3

@@ -50,7 +50,7 @@ ierror = throwError

50

51tclift :: TC a -> Idris a

52tclift (OK v) = return v

53−tclift (Error err@(At (FC f l) e)) = do setErrLine l ; throwError err

53+tclift (Error err@(At (FC f l c) e)) = do setErrLine l ; throwError err

54tclift (Error err) = throwError err

55

56tctry :: TC a -> TC a -> Idris a

@@ -60,7 +60,9 @@ tctry tc1 tc2

60 Error err -> tclift tc2

61

62getErrLine :: Err -> Int

63−getErrLine (At (FC _ l) _) = l

63+getErrLine (At (FC _ l _) _) = l

64getErrLine _ = 0

65

66−

66+getErrColumn :: Err -> Int

67+getErrColumn (At (FC _ _ c) _) = c

68+getErrColumn _ = 0

src/Idris/IBC.hs+5−3

@@ -23,7 +23,7 @@ import Debug.Trace

23import Paths_idris

24

25ibcVersion :: Word8

26−ibcVersion = 41

26+ibcVersion = 42

27

28data IBCFile = IBCFile { ver :: Word8,

29 sourcefile :: FilePath,

@@ -346,13 +346,15 @@ instance Binary CGInfo where

346 return (CGInfo x1 x2 x3 x4 x5)

347

348instance Binary FC where

349− put (FC x1 x2)

349+ put (FC x1 x2 x3)

350 = do put x1

351 put x2

352+ put x3

352 get

353 get

353 = do x1 <- get

354 = do x1 <- get

354 x2 <- get

355 x2 <- get

356+ x3 <- get

355− return (FC x1 x2)

357+ return (FC x1 x2 x3)

356

358

357

359

358instance Binary Name where

360instance Binary Name where

src/Idris/ParseHelpers.hs+7−1

@@ -254,13 +254,19 @@ fileName _ = "(interactive)"

254lineNum :: Delta -> Int

255lineNum (Lines l _ _ _) = fromIntegral l + 1

256lineNum (Directed _ l _ _ _) = fromIntegral l + 1

257+lineNum _ = 0

258+

259+{- | Get column number from position -}

260+columnNum :: Delta -> Int

261+columnNum pos = fromIntegral (column pos) + 1

262+

257

263

258{- | Get file position as FC -}

264{- | Get file position as FC -}

259getFC :: MonadicParsing m => m FC

265getFC :: MonadicParsing m => m FC

260getFC = do s <- position

266getFC = do s <- position

261 let (dir, file) = splitFileName (fileName s)

267 let (dir, file) = splitFileName (fileName s)

262 let f = if dir == addTrailingPathSeparator "." then file else fileName s

268 let f = if dir == addTrailingPathSeparator "." then file else fileName s

263− return $ FC f (lineNum s)

269+ return $ FC f (lineNum s) (columnNum s)

264

270

265{-* Syntax helpers-}

271{-* Syntax helpers-}

266-- | Bind constraints to term

272-- | Bind constraints to term

src/Idris/Parser.hs+1−1

@@ -1032,7 +1032,7 @@ loadSource lidr f

1032 toMutual :: PDecl -> PDecl

1033 toMutual m@(PMutual _ d) = m

1034 toMutual (PNamespace x ds) = PNamespace x (map toMutual ds)

1035− toMutual x = let r = PMutual (FC "single mutual" 0) [x] in

1035+ toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1036 case x of

1037 PClauses _ _ _ _ -> r

1038 PClass _ _ _ _ _ _ _ -> r

src/Idris/Prover.hs+2−2

@@ -65,9 +65,9 @@ prove ctxt lit n ty

65 ideslavePutSExp "end-proof-mode" n

66 let proofs = proof_list i

67 putIState (i { proof_list = (n, prf) : proofs })

68− let tree = simpleCase False True False CompileTime (FC "proof" 0) [([], P Ref n ty, tm)]

68+ let tree = simpleCase False True False CompileTime (fileFC "proof") [([], P Ref n ty, tm)]

69 logLvl 3 (show tree)

70− (ptm, pty) <- recheckC (FC "proof" 0) [] tm

70+ (ptm, pty) <- recheckC (fileFC "proof") [] tm

71 logLvl 5 ("Proof type: " ++ show pty ++ "\n" ++

72 "Expected type:" ++ show ty)

73 case converts ctxt [] ty pty of

src/Idris/REPL.hs+3−3

@@ -491,7 +491,7 @@ process fn (Prove n')

491 prover (lit fn) n

492 -- recheck totality

493 i <- getIState

494− totcheck (FC "(input)" 0, n)

494+ totcheck (fileFC "(input)", n)

495 mapM_ (\ (f,n) -> setTotality n Unchecked) (idris_totcheck i)

496 mapM_ checkDeclTotality (idris_totcheck i)

497

@@ -522,13 +522,13 @@ process fn Execute = do (m, _) <- elabVal toplevel False

522 compile t tmpn m

523 runIO $ system tmpn

524 return ()

525− where fc = FC "main" 0

525+ where fc = fileFC "main"

526process fn (Compile codegen f)

527 = do (m, _) <- elabVal toplevel False

528 (PApp fc (PRef fc (UN "run__IO"))

529 [pexp $ PRef fc (NS (UN "main") ["Main"])])

530 compile codegen f m

531− where fc = FC "main" 0

531+ where fc = fileFC "main"

532process fn (LogLvl i) = setLogLevel i

533-- Elaborate as if LHS of a pattern (debug command)

534process fn (Pattelab t)

src/Idris/Unlit.hs+2−2

@@ -24,8 +24,8 @@ check f l [x] = return ()

24check f l [] = return ()

25

26chkAdj :: FilePath -> Int -> LineType -> LineType -> TC ()

27−chkAdj f l Prog Comm = tfail $ At (FC f l) ProgramLineComment

27+chkAdj f l Prog Comm = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

28−chkAdj f l Comm Prog = tfail $ At (FC f l) ProgramLineComment

28+chkAdj f l Comm Prog = tfail $ At (FC f l 0) ProgramLineComment --TODO: Include column?

29chkAdj f l _ _ = return ()

30

31

test/reg003/expected+4−4

@@ -1,7 +1,7 @@

1−reg003a.idr:4:When elaborating constructor ECons:

1+reg003a.idr:4:20:When elaborating constructor ECons:

2No such variable OddList

3−reg003a.idr:7:When elaborating constructor OCons:

3+reg003a.idr:7:20:When elaborating constructor OCons:

4No such variable EvenList

5−reg003a.idr:9:When elaborating type of test:

5+reg003a.idr:9:8:When elaborating type of test:

6No such variable EvenList

7−reg003a.idr:10:No type declaration for test

7+reg003a.idr:10:1:No type declaration for test

test/reg006/expected+1−1

@@ -1 +1 @@

1−reg006.idr:17:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

1+reg006.idr:17:1:RBTree.lookup is possibly not total due to: RBTree.case block in lookup

test/reg007/expected+2−2

@@ -1,5 +1,5 @@

1−reg007.lidr:8:A.n is already defined

1+reg007.lidr:8:1:A.n is already defined

2−reg007.lidr:12:When elaborating right hand side of hurrah:

2+reg007.lidr:12:9:When elaborating right hand side of hurrah:

3Can't unify

4 [92mn[0m[94m = [0m[92mA.lala[0m

5with

test/reg010/expected+1−1

@@ -1,4 +1,4 @@

1−reg010.idr:5:When elaborating right hand side of usubst.unsafeSubst:

1+reg010.idr:5:15:When elaborating right hand side of usubst.unsafeSubst:

2Can't unify

3 P x

4with

test/reg018/expected+4−4

@@ -1,4 +1,4 @@

1−reg018a.idr:16:conat.minusCoNat is not productive

1+reg018a.idr:16:1:conat.minusCoNat is not productive

2−reg018b.idr:8:A.showB is possibly not total due to recursive path A.showB

2+reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

3−reg018c.idr:19:CodataTest.inf is not productive

3+reg018c.idr:19:1:CodataTest.inf is not productive

4−reg018d.idr:5:Main.pull is not total as there are missing cases

4+reg018d.idr:5:1:Main.pull is not total as there are missing cases

test/reg023/expected+1−1

@@ -1,4 +1,4 @@

1−reg023.idr:7:When elaborating right hand side of bad:

1+reg023.idr:7:5:When elaborating right hand side of bad:

2Can't unify

3 [94mNat[0m

4with

test/test003/expected+1−1

@@ -1,4 +1,4 @@

1−./test003a.lidr:1:Program line next to comment

1+./test003a.lidr:1:0:Program line next to comment

2a

3d

4zabcdefg

test/test010/expected+3−3

@@ -1,3 +1,3 @@

1−test010.idr:13:foo is possibly not total due to: MkBad

1+test010.idr:13:1:foo is possibly not total due to: MkBad

2−test010a.idr:9:main.bar is possibly not total due to: main.MkBad

2+test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

3−test010b.idr:9:main.bar is possibly not total due to: main.MkBad

3+test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

test/test012/expected+1−1

@@ -1 +1 @@

1−test012a.idr:7:x is not an accessible pattern variable

1+test012a.idr:7:1:x is not an accessible pattern variable

test/test017/expected+2−2

@@ -1,2 +1,2 @@

1−test017a.idr:5:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

1+test017a.idr:5:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

2−test017b.idr:4:foo.foo is possibly not total due to recursive path foo.foo

2+test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

test/test020/expected+1−1

@@ -1,5 +1,5 @@

1When elaborating right hand side of foo:

2−test020a.idr:14:Can't unify

2+test020a.idr:14:18:Can't unify

3 Vect n a

4with

5 List a

test/test030/expected+1−1

@@ -1,4 +1,4 @@

1−test030a.idr:12:When elaborating right hand side of testReflect1:

1+test030a.idr:12:14:When elaborating right hand side of testReflect1:

2Can't unify

3 IsJust (Just x)

4with