382542a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add %no_implicit directive

'implicit' is useful, but can cause problems when there are lots of places implicit coercions can be applied. In particular, in Effects, 'lift' can be applied to each operation, and to the combination of operations in >>=, so if there's an error the elaborator will try an exponentially increasing number of things depending on the number of >>=s. This is a bit of an ugly hack, but it allows certain definitions (such as >>=) to be non-coercible, so this exponential explosion doesn't happen any more. Fixes #1446

commit382542a3d482d2e835b5609f6d0d9e78f8d33d3e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 30 Jul 2014, 23:29 (12 years ago) parent8407c27

5 files changed+22

compare with master

unifiedsplit

libs/effects/Effects.idr+1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/ElabTerm.hs+14 src/Idris/IBC.hs+3 src/Idris/Parser.hs+3

libs/effects/Effects.idr+1

@@ -152,6 +152,7 @@ data Eff : (x : Type)

152152 Eff t [x] xs' -> -- [x] (\v => xs) ->

153153 Eff t [l ::: x] (\v => map (l :::) (xs' v))

154154

155+%no_implicit

155156(>>=) : Eff a xs xs' ->

156157 ((val : a) -> Eff b (xs' val) xs'') -> Eff b xs xs''

157158(>>=) = ebind

src/Idris/AbsSyntaxTree.hs+1

@@ -476,6 +476,7 @@ data FnOpt = Inlinable -- always evaluate when simplifying

476476 | Dictionary -- type class dictionary, eval only when

477477 -- a function argument, and further evaluation resutls

478478 | Implicit -- implicit coercion

479+ | NoImplicit -- do not apply implicit coercions

479480 | CExport String -- export, with a C name

480481 | ErrorHandler -- ^^ an error handler for use with the ErrorReflection extension

481482 | ErrorReverse -- ^^ attempt to reverse normalise before showing in error

src/Idris/ElabTerm.hs+14

@@ -855,9 +855,23 @@ elab ist info emode opts fn tm

855855 addImplBound ist (map fst env) (PApp fc (PRef fc (sUN "Delay"))

856856 [pexp t])

857857

858+

859+ -- Don't put implicit coercions around applications which are marked

860+ -- as '%noImplicit', or around case blocks, otherwise we get exponential

861+ -- blowup especially where there are errors deep in large expressions.

862+ notImplicitable (PApp _ f _) = notImplicitable f

863+ -- TMP HACK no coercing on bind (make this configurable)

864+ notImplicitable (PRef _ n)

865+ | [opts] <- lookupCtxt n (idris_flags ist)

866+ = NoImplicit `elem` opts

867+ notImplicitable (PAlternative True as) = any notImplicitable as

858868 -- case is tricky enough without implicit coercions! If they are needed,

859869 -- they can go in the branches separately.

870+ notImplicitable (PCase _ _ _) = True

871+ notImplicitable _ = False

872+

860873 insertCoerce ina t@(PCase _ _ _) = return t

874+ insertCoerce ina t | notImplicitable t = return t

861875 insertCoerce ina t =

862876 do ty <- goal

863877 -- Check for possible coercions to get to the goal

src/Idris/IBC.hs+3

@@ -274,6 +274,7 @@ process i fn

274274 pDefs (symbols i) (ibc_defs i)

275275 pPatdefs (ibc_patdefs i)

276276 pAccess (ibc_access i)

277+ pFlags (ibc_flags i)

277278 pTotal (ibc_total i)

278279 pTotCheckErr (ibc_totcheckfail i)

279280 pCG (ibc_cg i)

@@ -943,6 +944,7 @@ instance Binary FnOpt where

943944 ErrorHandler -> putWord8 9

944945 ErrorReverse -> putWord8 10

945946 CoveringFn -> putWord8 11

947+ NoImplicit -> putWord8 12

946948 get

947949 = do i <- getWord8

948950 case i of

@@ -959,6 +961,7 @@ instance Binary FnOpt where

959961 9 -> return ErrorHandler

960962 10 -> return ErrorReverse

961963 11 -> return CoveringFn

964+ 12 -> return NoImplicit

962965 _ -> error "Corrupted binary data for FnOpt"

963966

964967instance Binary Fixity where

src/Idris/Parser.hs+3

@@ -376,6 +376,7 @@ fnDecl' syn = checkFixity $

376376FnOpts ::= 'total'

377377 | 'partial'

378378 | 'implicit'

379+ | '%' 'no_implicit'

379380 | '%' 'assert_total'

380381 | '%' 'error_handler'

381382 | '%' 'reflection'

@@ -402,6 +403,8 @@ fnOpts opts

402403 <|> do reserved "covering"; fnOpts (CoveringFn : (opts \\ [TotalFn]))

403404 <|> do try (lchar '%' *> reserved "export"); c <- stringLiteral;

404405 fnOpts (CExport c : opts)

406+ <|> do try (lchar '%' *> reserved "no_implicit");

407+ fnOpts (NoImplicit : opts)

405408 <|> do try (lchar '%' *> reserved "assert_total");

406409 fnOpts (AssertTotal : opts)

407410 <|> do try (lchar '%' *> reserved "error_handler");