0ab30e7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Restrict error reflection scope to one argument

Now, error reflection can be applied to a single argument of a single function. It is triggered upon an error while elaborating applications. See test038 for an example.

commit0ab30e77ab65dacb412ec77dde0ab01d7df80c3d authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateThu 23 Jan 2014, 15:44 (13 years ago) parente9c9297

10 files changed+240−81

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntax.hs+18−8 src/Idris/AbsSyntaxTree.hs+2−1 src/Idris/Core/Elaborate.hs+18−13 src/Idris/ElabTerm.hs+90−52 src/Idris/Parser.hs+8−6 src/Idris/ProofSearch.hs+2−1 test/test038/FunErrTest.idr+49 test/test038/expected+47 test/test038/run+3

idris.cabal+3

@@ -309,6 +309,9 @@ Extra-source-files:

309309 test/test037/run

310310 test/test037/expected

311311 test/test037/*.idr

312+ test/test038/run

313+ test/test038/expected

314+ test/test038/*.idr

312315

313316source-repository head

314317 type: git

src/Idris/AbsSyntax.hs+18−8

@@ -25,6 +25,7 @@ import Data.List

2525import Data.Char

2626import qualified Data.Text as T

2727import Data.Either

28+import qualified Data.Map as M

2829import Data.Maybe

2930import qualified Data.Set as S

3031import Data.Word (Word)

@@ -149,14 +150,23 @@ addToCG n cg

149150 = do i <- getIState

150151 putIState $ i { idris_callgraph = addDef n cg (idris_callgraph i) }

151152

152−-- | Adds hs as error handlers for n. If n is ambiguous, all matching ns are updated.

153−addFunctionErrorHandlers :: Name -> [Name] -> Idris ()

154−addFunctionErrorHandlers n hs = do i <- getIState

155− let currentHandlers = idris_function_errorhandlers i

156− let newHandlers = updateDef n

157− (\handlers -> handlers `S.union` S.fromList hs)

158− currentHandlers

159− putIState $ i { idris_function_errorhandlers = newHandlers }

153+-- | Adds error handlers for a particular function and argument. If names are is ambiguous, all matching handlers are updated.

154+addFunctionErrorHandlers :: Name -> Name -> [Name] -> Idris ()

155+addFunctionErrorHandlers f arg hs =

156+ do i <- getIState

157+ let oldHandlers = idris_function_errorhandlers i

158+ let newHandlers = flip (addDef f) oldHandlers $

159+ case lookupCtxtExact f oldHandlers of

160+ Nothing -> M.singleton arg (S.fromList hs)

161+ Just (oldHandlers) -> M.insertWith S.union arg (S.fromList hs) oldHandlers

162+ -- will always be one of those two, thus no extra case

163+ putIState $ i { idris_function_errorhandlers = newHandlers }

164+

165+getFunctionErrorHandlers :: Name -> Name -> Idris [Name]

166+getFunctionErrorHandlers f arg = do i <- getIState

167+ return . maybe [] S.toList $

168+ undefined --lookup arg =<< lookupCtxtExact f (idris_function_errorhandlers i)

169+

160170

161171-- Trace all the names in a call graph starting at the given name

162172getAllNames :: Name -> Idris [Name]

src/Idris/AbsSyntaxTree.hs+2−1

@@ -24,6 +24,7 @@ import Control.Monad.Trans.Error

2424

2525import Data.List

2626import Data.Char

27+import qualified Data.Map as M

2728import qualified Data.Text as T

2829import Data.Either

2930import qualified Data.Set as S

@@ -136,7 +137,7 @@ data IState = IState {

136137 idris_outh :: Handle,

137138 idris_errorhandlers :: [Name], -- ^ Global error handlers

138139 idris_nameIdx :: (Int, Ctxt (Int, Name)),

139− idris_function_errorhandlers :: Ctxt (S.Set Name) -- ^ Specific error handlers

140+ idris_function_errorhandlers :: Ctxt (M.Map Name (S.Set Name)) -- ^ Specific error handlers

140141 }

141142

142143data SizeChange = Smaller | Same | Bigger | Unknown

src/Idris/Core/Elaborate.hs+18−13

@@ -401,8 +401,11 @@ qed = do processTactic' QED

401401undo :: Elab' aux ()

402402undo = processTactic' Undo

403403

404−prepare_apply :: Raw -> [Bool] -> Elab' aux [Name]

405−prepare_apply fn imps =

404+-- | Prepare to apply a function by creating holes to be filled by the arguments

405+prepare_apply :: Raw -- ^ The operation being applied

406+ -> [Bool] -- ^ Whether arguments are implicit

407+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes to be filled with elaborated argument values

408+prepare_apply fn imps =

406409 do ty <- get_type fn

407410 ctxt <- get_context

408411 env <- get_env

@@ -414,11 +417,13 @@ prepare_apply fn imps =

414417 let n = length (filter not imps)

415418 let (h : hs) = holes p

416419 put (ES (p { holes = h : (reverse (take n hs) ++ drop n hs) }, a) s prev)

417−-- case claims of

418−-- [] -> return ()

419−-- (h : _) -> reorder_claims h

420420 return $! claims

421421 where

422+ mkClaims :: Type -- ^ The type of the operation being applied

423+ -> [Bool] -- ^ Whether the arguments are implicit

424+ -> [(Name, Name)] -- ^ Accumulator for produced claims

425+ -> [Name] -- ^ Hypotheses

426+ -> Elab' aux [(Name, Name)] -- ^ The names of the arguments and their holes, resp.

422427 mkClaims (Bind n' (Pi t_in) sc) (i : is) claims hs =

423428 do let t = rebind hs t_in

424429 n <- getNameFrom (mkMN n')

@@ -427,7 +432,7 @@ prepare_apply fn imps =

427432-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

428433 claim n (forget t)

429434 when i (movelast n)

430− mkClaims sc' is (n : claims) hs

435+ mkClaims sc' is ((n', n) : claims) hs

431436 mkClaims t [] claims _ = return $! (reverse claims)

432437 mkClaims _ _ _ _

433438 | Var n <- fn

@@ -452,11 +457,11 @@ prepare_apply fn imps =

452457 rebind hs (App f a) = App (rebind hs f) (rebind hs a)

453458 rebind hs t = t

454459

455−apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [Name]

460+apply, match_apply :: Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

456461apply = apply' fill

457462match_apply = apply' match_fill

458463

459−apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [Name]

464+apply' :: (Raw -> Elab' aux ()) -> Raw -> [(Bool, Int)] -> Elab' aux [(Name, Name)]

460465apply' fillt fn imps =

461466 do args <- prepare_apply fn (map fst imps)

462467 -- _Don't_ solve the arguments we're specifying by hand.

@@ -468,7 +473,7 @@ apply' fillt fn imps =

468473 let dont = head hs : dontunify p ++

469474 if null imps then [] -- do all we can

470475 else

471− map fst (filter (not.snd) (zip args (map fst imps)))

476+ map fst (filter (not . snd) (zip (map snd args) (map fst imps)))

472477 let (n, hunis) = -- trace ("AVOID UNIFY: " ++ show (fn, dont) ++ "\n" ++ show ptm) $

473478 unified p

474479 let unify = -- trace ("Not done " ++ show hs) $

@@ -477,10 +482,10 @@ apply' fillt fn imps =

477482 keepGiven dont hunis hs

478483 put (ES (p { dontunify = dont, unified = (n, unify),

479484 notunified = notunify ++ notunified p }, a) s prev)

480− fillt (raw_apply fn (map Var args))

485+ fillt (raw_apply fn (map (Var . snd) args))

481486-- trace ("Goal " ++ show g ++ "\n" ++ show (fn, imps, unify) ++ "\n" ++ show ptm) $

482487 end_unify

483− return $! (map (updateUnify unify) args)

488+ return $! (map (\(argName, argHole) -> (argName, updateUnify unify argHole)) args)

484489 where updateUnify us n = case lookup n us of

485490 Just (P _ t _) -> t

486491 _ -> n

@@ -488,8 +493,8 @@ apply' fillt fn imps =

488493apply2 :: Raw -> [Maybe (Elab' aux ())] -> Elab' aux ()

489494apply2 fn elabs =

490495 do args <- prepare_apply fn (map isJust elabs)

491− fill (raw_apply fn (map Var args))

492− elabArgs args elabs

496+ fill (raw_apply fn (map (Var . snd) args))

497+ elabArgs (map snd args) elabs

493498 ES (p, a) s prev <- get

494499 let (n, hs) = unified p

495500 end_unify

src/Idris/ElabTerm.hs+90−52

@@ -13,10 +13,14 @@ import Idris.Core.TT

1313import Idris.Core.Evaluate

1414import Idris.Core.Typecheck (check)

1515

16+import Control.Applicative ((<$>))

1617import Control.Monad

1718import Control.Monad.State.Strict

1819import Data.List

20+import qualified Data.Map as M

1921import Data.Maybe (mapMaybe)

22+import qualified Data.Set as S

23+import qualified Data.Text as T

2024

2125import Debug.Trace

2226

@@ -396,7 +400,7 @@ elab ist info pattern opts fn tm

396400 solve

397401 elab' (_, _, inty) (PApp fc (PRef _ f) args')

398402 | isTConName f (tt_ctxt ist) && pattern && not reflect && not inty

399− = lift $ tfail (Msg "Typecase is not allowed")

403+ = lift $ tfail (Msg "Typecase is not allowed")

400404 -- if f is local, just do a simple_app

401405 elab' (ina, g, inty) tm@(PApp fc (PRef _ f) args)

402406 = do env <- get_env

@@ -419,12 +423,14 @@ elab ist info pattern opts fn tm

419423 _ -> mapM_ setInjective (map getTm args)

420424 ctxt <- get_context

421425 let guarded = isConName f ctxt

426+-- trace ("args is " ++ show args) $ return ()

422427 ns <- apply (Var f) (map isph args)

428+-- trace ("ns is " ++ show ns) $ return ()

423429 -- Sort so that the implicit tactics and alternatives go last

424430 let (ns', eargs) = unzip $

425431 sortBy cmpArg (zip ns args)

426− elabArgs (ina || not isinf, guarded, inty)

427− [] fc False ns' (map (\x -> (lazyarg x, getTm x)) eargs)

432+ elabArgs ist (ina || not isinf, guarded, inty)

433+ [] fc False f ns' (map (\x -> (lazyarg x, getTm x)) eargs)

428434 solve

429435 ivs' <- get_instances

430436 -- Attempt to resolve any type classes which have 'complete' types,

@@ -613,45 +619,73 @@ elab ist info pattern opts fn tm

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

614620

615621 -- | Elaborate the arguments to a function

616− elabArgs :: (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

622+ elabArgs :: IState -- ^ The current Idris state

623+ -> (Bool, Bool, Bool) -- ^ (in an argument, guarded, in a type)

617624 -> [Bool]

618625 -> FC -- ^ Source location

619626 -> Bool

620− -> [Name] -- ^ Names of arguments - these identify the holes to be filled

627+ -> Name -- ^ Name of the function being applied

628+ -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

621629 -> [(Bool, PTerm)] -- ^ (Laziness, argument)

622630 -> ElabD ()

623− elabArgs ina failed fc retry [] _

631+ elabArgs ist ina failed fc retry f [] _

624632-- | retry = let (ns, ts) = unzip (reverse failed) in

625633-- elabArgs ina [] False ns ts

626634 | otherwise = return ()

627− elabArgs ina failed fc r (n:ns) ((_, Placeholder) : args)

628− = elabArgs ina failed fc r ns args

629− elabArgs ina failed fc r (n:ns) ((lazy, t) : args)

635+ elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args)

636+ = elabArgs ist ina failed fc r f ns args

637+ elabArgs ist ina failed fc r f ((argName, holeName):ns) ((lazy, t) : args)

630638 | lazy && not pattern

631− = do elabArg n (PApp bi (PRef bi (sUN "lazy"))

632− [pimp (sUN "a") Placeholder True,

633− pexp t]);

634− | otherwise = elabArg n t

635− where elabArg n t

636− = do hs <- get_holes

637− tm <- get_term

638− failed' <- -- trace (show (n, t, hs, tm)) $

639− -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

640− case n `elem` hs of

641− True -> do focus n; elabE ina t; return failed

642− False -> return failed

643− elabArgs ina failed fc r ns args

644−

645−-- | Perform error reflection for functions with specific error handlers

646−reflectFunctionErrors :: IState -> Name -> ElabD a -> ElabD a

647−reflectFunctionErrors ist f action =

639+ = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

640+ [pimp (sUN "a") Placeholder True,

641+ pexp t])

642+ | otherwise = elabArg argName holeName t

643+ where elabArg argName holeName t =

644+ reflectFunctionErrors ist f argName $

645+ do hs <- get_holes

646+ tm <- get_term

647+ failed' <- -- trace (show (n, t, hs, tm)) $

648+ -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

649+ case holeName `elem` hs of

650+ True -> do focus holeName; elabE ina t; return failed

651+ False -> return failed

652+ elabArgs ist ina failed fc r f ns args

653+

654+-- | Perform error reflection for function applicaitons with specific error handlers

655+reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a

656+reflectFunctionErrors ist f arg action =

648657 do elabState <- get

649658 (result, newState) <- case runStateT action elabState of

650659 OK (res, newState) -> return (res, newState)

651− Error e -> lift (tfail e) -- TODO: actual error reflection!

660+ Error e@(ReflectionError _ _) -> (lift . tfail) e

661+ Error e@(ReflectionFailed _ _) -> (lift . tfail) e

662+ Error e -> handle e >>= lift . tfail

652663 put newState

653664 return result

665+ where handle :: Err -> ElabD Err

666+ handle e = do let funhandlers = (maybe M.empty id . lookupCtxtExact f . idris_function_errorhandlers) ist

667+ handlers = (maybe [] S.toList . M.lookup arg) funhandlers

668+ reports = map (\n -> RApp (Var n) (reflectErr e)) handlers

669+

670+

671+ -- Typecheck error handlers - if this fails, then something else was wrong earlier!

672+ handlers <- case mapM (check (tt_ctxt ist) []) reports of

673+ Error e -> lift . tfail $

674+ ReflectionFailed "Type error while constructing reflected error" e

675+ OK hs -> return hs

654676

677+ -- Normalize error handler terms to produce the new messages

678+ let ctxt = tt_ctxt ist

679+ results = map (normalise ctxt []) (map fst handlers)

680+

681+ -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

682+ let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

683+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

684+ Left err -> lift (tfail err)

685+ Right ok -> return ok

686+ return $ case errorparts of

687+ [] -> e

688+ parts -> ReflectionError errorparts e

655689

656690-- For every alternative, look at the function at the head. Automatically resolve

657691-- any nested alternatives where that function is also at the head

@@ -788,8 +822,8 @@ resolveTC depth topg fn ist

788822 [args] -> map isImp (snd args) -- won't be overloaded!

789823 ps <- get_probs

790824 tm <- get_term

791− args <- try' (apply (Var n) imps)

792− (match_apply (Var n) imps) True

825+ args <- map snd <$> try' (apply (Var n) imps)

826+ (match_apply (Var n) imps) True

793827 ps' <- get_probs

794828 when (length ps < length ps') $ fail "Can't apply type class"

795829-- traceWhen (all boundVar ttypes) ("Progress: " ++ show t ++ " with " ++ show n) $

@@ -802,7 +836,7 @@ resolveTC depth topg fn ist

802836 -- if there's any arguments left, we've failed to resolve

803837 hs <- get_holes

804838 ulog <- getUnifyLog

805− solve

839+ solve

806840 traceWhen ulog ("Got " ++ show n) $ return ()

807841 where isImp (PImp p _ _ _ _ _) = (True, p)

808842 isImp arg = (False, priority arg)

@@ -1487,6 +1521,7 @@ reflectErr (LoadingFailed str err) =

14871521 raw_apply (Var $ reflErrName "LoadingFailed") [RConstant (Str str)]

14881522reflectErr x = raw_apply (Var (sNS (sUN "Msg") ["Errors", "Reflection", "Language"])) [RConstant . Str $ "Default reflection: " ++ show x]

14891523

1524+

14901525withErrorReflection :: Idris a -> Idris a

14911526withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

14921527 where handle :: Err -> Idris Err

@@ -1512,47 +1547,50 @@ withErrorReflection x = idrisCatch x (\ e -> handle e >>= ierror)

15121547

15131548 -- For each handler term output, either discard it if it is Nothing or reify it the Haskell equivalent

15141549 let errorpartsTT = mapMaybe unList (mapMaybe fromTTMaybe results)

1515− errorparts <- mapM (mapM reifyReportPart) errorpartsTT

1516−

1550+ errorparts <- case mapM (mapM reifyReportPart) errorpartsTT of

1551+ Left err -> ierror err

1552+ Right ok -> return ok

15171553 return $ case errorparts of

15181554 [] -> e

15191555 parts -> ReflectionError errorparts e

15201556

1521− fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1522− fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1523− | just == txt "Just" = Just tm

1524− fromTTMaybe x = Nothing

1557+fromTTMaybe :: Term -> Maybe Term -- WARNING: Assumes the term has type Maybe a

1558+fromTTMaybe (App (App (P (DCon _ _) (NS (UN just) _) _) ty) tm)

1559+ | just == txt "Just" = Just tm

1560+fromTTMaybe x = Nothing

15251561

15261562reflErrName :: String -> Name

15271563reflErrName n = sNS (sUN n) ["Errors", "Reflection", "Language"]

15281564

1529−reifyReportPart :: Term -> Idris ErrorReportPart

1565+-- | Attempt to reify a report part from TT to the internal

1566+-- representation. Not in Idris or ElabD monads because it should be usable

1567+-- from either.

1568+reifyReportPart :: Term -> Either Err ErrorReportPart

15301569reifyReportPart (App (P (DCon _ _) n _) (Constant (Str msg))) | n == reflErrName "TextPart" =

1531− return (TextPart msg)

1570+ Right (TextPart msg)

15321571reifyReportPart (App (P (DCon _ _) n _) ttn)

15331572 | n == reflErrName "NamePart" =

15341573 case runElab [] (reifyTTName ttn) (initElaborator NErased initContext Erased) of

1535− Error e -> ierror . InternalMsg $

1574+ Error e -> Left . InternalMsg $

15361575 "could not reify name term " ++

15371576 show ttn ++

15381577 " when reflecting an error"

1539− OK (n', _)-> return $ NamePart n'

1578+ OK (n', _)-> Right $ NamePart n'

15401579reifyReportPart (App (P (DCon _ _) n _) tm)

15411580 | n == reflErrName "TermPart" =

1542− do ist <- getIState

1543− case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1544− Error e -> ierror . InternalMsg $

1545− "could not reify reflected term " ++

1546− show tm ++

1547− " when reflecting an error"

1548− OK (tm', _) -> return $ TermPart tm'

1581+ case runElab [] (reifyTT tm) (initElaborator NErased initContext Erased) of

1582+ Error e -> Left . InternalMsg $

1583+ "could not reify reflected term " ++

1584+ show tm ++

1585+ " when reflecting an error"

1586+ OK (tm', _) -> Right $ TermPart tm'

15491587reifyReportPart (App (P (DCon _ _) n _) tm)

15501588 | n == reflErrName "SubReport" =

1551− case unList tm of

1552− Just xs -> do subParts <- mapM reifyReportPart xs

1553− return (SubReport subParts)

1554− Nothing -> ierror . InternalMsg $ "could not reify subreport " ++ show tm

1555−reifyReportPart x = ierror . InternalMsg $ "could not reify " ++ show x

1589+ case unList tm of

1590+ Just xs -> do subParts <- mapM reifyReportPart xs

1591+ Right (SubReport subParts)

1592+ Nothing -> Left . InternalMsg $ "could not reify subreport " ++ show tm

1593+reifyReportPart x = Left . InternalMsg $ "could not reify " ++ show x

15561594

15571595envTupleType :: Raw

15581596envTupleType

src/Idris/Parser.hs+8−6

@@ -55,6 +55,7 @@ import Data.Char

5555import qualified Data.HashSet as HS

5656import qualified Data.Text as T

5757import qualified Data.ByteString.UTF8 as UTF8

58+import qualified Data.Set as S

5859

5960import Debug.Trace

6061

@@ -870,15 +871,16 @@ directive syn = do try (lchar '%' *> reserved "lib"); cgn <- codegen_; lib <- st

870871 <|> do try (lchar '%' *> reserved "name")

871872 ty <- iName []

872873 ns <- sepBy1 name (lchar ',')

873− return [PDirective

874− (do ty' <- disambiguate ty

875− mapM_ (addNameHint ty') ns

876− mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

874+ return [PDirective (do ty' <- disambiguate ty

875+ mapM_ (addNameHint ty') ns

876+ mapM_ (\n -> addIBC (IBCNameHint (ty', n))) ns)]

877877 <|> do try (lchar '%' *> reserved "error_handlers")

878878 fn <- iName []

879+ arg <- iName []

879880 ns <- sepBy1 name (lchar ',')

880− return [PDirective $ do n' <- disambiguate fn

881− addFunctionErrorHandlers fn ns]

881+ return [PDirective (do fn' <- disambiguate fn

882+ ns' <- mapM disambiguate ns

883+ addFunctionErrorHandlers fn' arg ns')]

882884 <|> do try (lchar '%' *> reserved "language"); ext <- pLangExt;

883885 return [PDirective (addLangExt ext)]

884886 <?> "directive"

src/Idris/ProofSearch.hs+2−1

@@ -10,6 +10,7 @@ import Idris.AbsSyntax

1010import Idris.Delaborate

1111import Idris.Error

1212

13+import Control.Applicative ((<$>))

1314import Control.Monad

1415import Debug.Trace

1516

@@ -86,7 +87,7 @@ proofSearch elab fn nroot hints ist = psRec maxDepth

8687 [args] -> map isImp (snd args)

8788 _ -> fail "Ambiguous name"

8889 ps <- get_probs

89− args <- apply (Var n) imps

90+ args <- map snd <$> apply (Var n) imps

9091 ps' <- get_probs

9192 when (length ps < length ps') $ fail "Can't apply constructor"

9293 mapM_ (\ (_, h) -> do focus h

test/test038/FunErrTest.idrnew file+49

@@ -0,0 +1,49 @@

1+module FunErrTest

3+import Language.Reflection

4+import Language.Reflection.Errors

5+import Language.Reflection.Utils

7+%language ErrorReflection

9+total

10+cadr : (xs : List a)

11+ -> {auto cons1 : isCons xs = True}

12+ -> {auto cons2 : isCons (tail xs cons1) = True}

13+ -> a

14+cadr (x :: (y :: _)) {cons1=refl} {cons2=refl} = y

15+cadr (x :: []) {cons1=refl} {cons2=refl} impossible

16+

17+total

18+eltsErr : TT -> TT -> Maybe (List ErrorReportPart)

19+eltsErr (P (DCon _ _) (NS (UN "False") _) _) (P (DCon _ _) (NS (UN "True") _) _) =

20+ Just [ NamePart (NS (UN "cadr") ["FunErrTest"])

21+ , TextPart "requires that its argument contain at least two elements."

22+ ]

23+eltsErr (P (DCon _ _) (NS (UN "True") _) _) (App (App isCons ty) xs) =

24+ Just [ NamePart (NS (UN "cadr") ["FunErrTest"])

25+ , TextPart "requires that its argument contain at least two elements."

26+ , TextPart "This fails because: "

27+ , SubReport [ TextPart "There is no proof that"

28+ , TermPart xs

29+ , TextPart "is non-empty."

30+ ]

31+ ]

32+eltsErr _ _ = Nothing

33+

34+total

35+has2elts : Err -> Maybe (List ErrorReportPart)

36+has2elts (CantUnify _ tm1 tm2 e _ _) = eltsErr tm1 tm2 <|> has2elts e

37+has2elts e = Just [TextPart (show e)]

38+

39+%error_handlers cadr cons1 has2elts

40+%error_handlers cadr cons2 has2elts

41+

42+problem1 : List a -> a

43+problem1 xs = cadr xs

44+

45+problem2 : Int

46+problem2 = cadr [1]

47+

48+problem3 : Int

49+problem3 = cadr []

test/test038/expectednew file+47

@@ -0,0 +1,47 @@

1+FunErrTest.idr:43:10:When elaborating right hand side of problem1:

2+FunErrTest.cadr requires that its argument contain at least two elements. This fails because:

3+ There is no proof that xs is non-empty.

5+Original error:

7+ Can't unify

8+ True = True

9+ with

10+ isCons xs = True

11+

12+ Specifically:

13+ Can't unify

14+ True

15+ with

16+ isCons xs

17+

18+FunErrTest.idr:46:10:When elaborating right hand side of problem2:

19+FunErrTest.cadr requires that its argument contain at least two elements.

20+Original error:

21+

22+ Can't unify

23+ x = x

24+ with

25+ False = True

26+

27+ Specifically:

28+ Can't unify

29+ False

30+ with

31+ True

32+

33+FunErrTest.idr:49:10:When elaborating right hand side of problem3:

34+FunErrTest.cadr requires that its argument contain at least two elements.

35+Original error:

36+

37+ Can't unify

38+ x = x

39+ with

40+ False = True

41+

42+ Specifically:

43+ Can't unify

44+ False

45+ with

46+ True

47+

test/test038/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ FunErrTest.idr --nocolour --check

3+rm -f *.ibc