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

git.iko.soy/Idris-dev

Restrict (and speed up) implicit coercions

'implicit' will now only work if there is a concrete argument type and a concrete return type. This means we can rule out impossible coercions much quicker, and has the effect of speeding up error reporting by not trying to fix up the error with coercions which are never going to work. There's a special case for "lend" but UniqueType is experimental and probably needs a rethink, so I'm okay with this at least for now.

commit0dd2f066b0eb865512c6153eeb5163195ba9599a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 17 Jul 2015, 12:14 (11 years ago) parent3166b15

4 files changed+70−6

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Elaborate.hs+5−3 src/Idris/Elab/Term.hs+62−3 src/Idris/IBC.hs+2

src/Idris/AbsSyntaxTree.hs+1

@@ -877,6 +877,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

877877

878878data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

879879 | FirstSuccess

880+ | TryImplicit

880881 deriving (Eq, Data, Typeable)

881882

882883-- | Transform the FCs in a PTerm. The first function transforms the

src/Idris/Core/Elaborate.hs+5−3

@@ -812,9 +812,10 @@ tryCatch t1 t2

812812 = do s <- get

813813 ps <- get_probs

814814 ulog <- getUnifyLog

815− case prunStateT 999999 False ps t1 s of

816− OK ((v, _, _), s') -> do put s'

817− return $! v

815+-- case prunStateT 999999 False ps t1 s of

816+ case runStateT t1 s of

817+ OK (v, s') -> do put s'

818+ return $! v

818819 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

819820 case runStateT (t2 e1) s of

820821 OK (v, s') -> do put s'

@@ -863,6 +864,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

863864 if (s >= i) then (lift (tfail err), s)

864865 else (f, i)

865866

867+-- Run an elaborator, and fail if any problems are introduced

866868prunStateT

867869 :: Int

868870 -> Bool

src/Idris/Elab/Term.hs+62−3

@@ -479,6 +479,66 @@ elab ist info emode opts fn tm

479479 trySeq' deferr (x : xs)

480480 = try' (do elab' ina fc x

481481 solveAutos ist fn False) (trySeq' deferr xs) True

482+ elab' ina fc (PAlternative TryImplicit (orig : alts)) = do

483+ env <- get_env

484+ let doelab = elab' ina fc orig

485+ tryCatch doelab

486+ (\err ->

487+ if recoverableErr err

488+ then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

489+ -- show alts ++ "\n" ++

490+ -- showQuick err) $

491+ -- Prune the coercions so that only the ones

492+ -- with the right type to fix the error will be tried!

493+ case pruneAlts err alts env of

494+ [] -> lift $ tfail err

495+ alts' ->

496+ try' (elab' ina fc (PAlternative (ExactlyOne False) alts'))

497+ (lift $ tfail err) -- take error from original if all fail

498+ True

499+ else lift $ tfail err)

500+ where

501+ recoverableErr (CantUnify _ _ _ _ _ _) = True

502+ recoverableErr (CantSolveGoal _ _) = False

503+ recoverableErr (CantResolveAlts _) = False

504+ recoverableErr (ProofSearchFail (Msg _)) = True

505+ recoverableErr (ProofSearchFail _) = False

506+ recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

507+ recoverableErr (At _ e) = recoverableErr e

508+ recoverableErr (ElabScriptDebug _ _ _) = False

509+ recoverableErr _ = True

510+

511+ pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env

512+ = case unApply (normalise (tt_ctxt ist) env inc) of

513+ (P (TCon _ _) n _, _) -> filter (hasArg n env) alts

514+ (Constant _, _) -> alts

515+ _ -> filter isLend alts -- special case hack for 'Borrowed'

516+ pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

517+ pruneAlts (At _ e) alts env = pruneAlts e alts env

518+ pruneAlts _ alts _ = filter isLend alts

519+

520+ hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

521+ hasArg n env (PApp _ (PRef _ a) _)

522+ = case lookupTyExact a (tt_ctxt ist) of

523+ Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

524+ any (fnIs n) args

525+ Nothing -> False

526+ hasArg n _ _ = False

527+

528+ isLend (PApp _ (PRef _ l) _) = l == sNS (sUN "lend") ["Ownership"]

529+ isLend _ = False

530+

531+ fnIs n ty = case unApply ty of

532+ (P _ n' _, _) -> n == n'

533+ _ -> False

534+

535+ showQuick (CantUnify _ (l, _) (r, _) _ _ _)

536+ = show (l, r)

537+ showQuick (ElaboratingArg _ _ _ e) = showQuick e

538+ showQuick (At _ e) = showQuick e

539+ showQuick (ProofSearchFail (Msg _)) = "search fail"

540+ showQuick _ = "No chance"

541+

482542 elab' ina _ (PPatvar fc n) | bindfree

483543 = do patvar n

484544 update_term liftPats

@@ -1299,9 +1359,8 @@ elab ist info emode opts fn tm

12991359 let t' = case (t, cs) of

13001360 (PCoerced tm, _) -> tm

13011361 (_, []) -> t

1302− (_, cs) -> PAlternative FirstSuccess [t ,

1303− PAlternative (ExactlyOne False)

1304− (map (mkCoerce env t) cs)]

1362+ (_, cs) -> PAlternative TryImplicit

1363+ (t : map (mkCoerce env t) cs)

13051364 return t'

13061365 where

13071366 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

src/Idris/IBC.hs+2

@@ -1801,12 +1801,14 @@ instance Binary PAltType where

18011801 ExactlyOne x1 -> do putWord8 0

18021802 put x1

18031803 FirstSuccess -> putWord8 1

1804+ TryImplicit -> putWord8 2

18041805 get

18051806 = do i <- getWord8

18061807 case i of

18071808 0 -> do x1 <- get

18081809 return (ExactlyOne x1)

18091810 1 -> return FirstSuccess

1811+ 2 -> return TryImplicit

18101812 _ -> error "Corrupted binary data for PAltType"

18111813

18121814