26cfbe9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Scoped implicits fix

If after an application there are more implicit arguments expected, add those arguments then re-elaborate the application - we often don't know what these arguments will be until after elaborating the application because the application itself may compute a type. Fixes #1899

commit26cfbe9e1eb37eec97d4447ead813a261d386dc8 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 14 Feb 2015, 13:58 (12 years ago) parentcdfaa9f

14 files changed+144−48

compare with master

unifiedsplit

idris.cabal+3 libs/effects/Effects.idr+1 src/Idris/AbsSyntaxTree.hs+1 src/Idris/Core/Elaborate.hs+4−4 src/Idris/Core/ProofState.hs+6−4 src/Idris/Core/TT.hs+3 src/Idris/Core/Unify.hs+3−3 src/Idris/DeepSeq.hs+1 src/Idris/ElabTerm.hs+83−37 src/Idris/IBC.hs+1 test/reg058/expected test/reg058/implicits.idr+14 test/reg058/implicits2.idr+19 test/reg058/run+5

idris.cabal+3

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

286286 test/reg057/run

287287 test/reg057/*.idr

288288 test/reg057/expected

289+ test/reg058/run

290+ test/reg058/*.idr

291+ test/reg058/expected

289292

290293 test/basic001/run

291294 test/basic001/*.idr

libs/effects/Effects.idr+1

@@ -310,4 +310,5 @@ when : Bool -> Lazy ({xs} Eff ()) -> {xs} Eff ()

310310when True e = Force e

311311when False e = pure ()

312312

313+

313314-- --------------------------------------------------------------------- [ EOF ]

src/Idris/AbsSyntaxTree.hs+1

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

757757 | PLet FC Name PTerm PTerm PTerm -- ^ A let binding

758758 | PTyped PTerm PTerm -- ^ Term with explicit type

759759 | PApp FC PTerm [PArg] -- ^ e.g. IO (), List Char, length x

760+ | PAppImpl PTerm [ImplicitInfo] -- ^ Implicit argument application (introduced during elaboration only)

760761 | PAppBind FC PTerm [PArg] -- ^ implicitly bound application

761762 | PMatchApp FC Name -- ^ Make an application by type matching

762763 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

src/Idris/Core/Elaborate.hs+4−4

@@ -234,7 +234,7 @@ is_guess = do ES p _ _ <- get

234234 _ -> return False

235235

236236-- Get the guess at the current hole, if there is one

237−get_guess :: Elab' aux Type

237+get_guess :: Elab' aux Term

238238get_guess = do ES p _ _ <- get

239239 b <- lift $ goalAtFocus (fst p)

240240 case b of

@@ -674,7 +674,7 @@ checkPiGoal n

674674 focus f

675675

676676simple_app :: Bool -> Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

677−simple_app infer fun arg app0str =

677+simple_app infer fun arg str =

678678 do a <- getNameFrom (sMN 0 "argTy")

679679 b <- getNameFrom (sMN 0 "retTy")

680680 f <- getNameFrom (sMN 0 "f")

@@ -705,8 +705,8 @@ simple_app infer fun arg app0str =

705705 when (a `elem` hs) $ do movelast a

706706 when (b `elem` hs) $ do movelast b

707707 end_unify

708− where regretWith err = try regret

709− (lift $ tfail err)

708+ where

709+ regretWith err = try regret (lift $ tfail err)

710710

711711-- Abstract over an argument of unknown type, giving a name for the hole

712712-- which we'll fill with the argument type too.

src/Idris/Core/ProofState.hs+6−4

@@ -853,6 +853,7 @@ updateProblems ps updates probs = up updates probs where

853853 hs = holes ps

854854 inj = injective ps

855855 ctxt = context ps

856+ ulog = unifylog ps

856857 usupp = map fst (notunified ps)

857858

858859 up ns [] = (ns, [])

@@ -864,8 +865,8 @@ updateProblems ps updates probs = up updates probs where

864865 if newx || newy || ready ||

865866 any (\n -> n `elem` inj) (refsIn x ++ refsIn y) then

866867 case unify ctxt env' x' y' inj hs usupp while of

867− OK (v, []) -> -- trace ("DID " ++ show (x',y',ready,v)) $

868− up (ns ++ v) ps

868+ OK (v, []) -> traceWhen ulog ("DID " ++ show (x',y',ready,v)) $

869+ up (ns ++ v) ps

869870 e -> -- trace ("FAILED " ++ show (x',y',ready,e)) $

870871 let (ns', ps') = up ns ps in

871872 (ns', (x',y', False, env',err', while, um) : ps')

@@ -966,7 +967,9 @@ processTactic t ps

966967 -- apply them here

967968 let ns' = dropGiven (dontunify ps') ns_in (holes ps')

968969 let pterm'' = updateSolved ns' (pterm ps')

969− traceWhen (unifylog ps) ("(Toplevel) Dropping holes: " ++ show (map fst ns')) $

970+ traceWhen (unifylog ps)

971+ ("Updated problems after solve " ++ qshow probs' ++ "\n" ++

972+ "(Toplevel) Dropping holes: " ++ show (map fst ns')) $

970973 return (ps' { pterm = pterm'',

971974 solved = Nothing,

972975 problems = probs',

@@ -989,7 +992,6 @@ process t h = tactic (Just h) (mktac t)

989992 mktac (MatchFill r) = match_fill r

990993 mktac (PrepFill n ns) = prep_fill n ns

991994 mktac CompleteFill = complete_fill

992− mktac Regret = regret

993995 mktac Solve = solve

994996 mktac (StartUnify n) = start_unify n

995997 mktac Compute = compute

src/Idris/Core/TT.hs+3

@@ -1345,6 +1345,8 @@ showEnv' env t dbg = se 10 env t where

13451345 = (show $ fst $ env!!i) ++

13461346 if dbg then "{" ++ show i ++ "}" else ""

13471347 | otherwise = "!!V " ++ show i ++ "!!"

1348+ se p env (Bind n b@(Pi (Just _) t k) sc)

1349+ = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

13481350 se p env (Bind n b@(Pi _ t k) sc)

13491351 | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

13501352 where arrow (TType _) = " -> "

@@ -1361,6 +1363,7 @@ showEnv' env t dbg = se 10 env t where

13611363 sb env n (Lam t) = showb env "\\ " " => " n t

13621364 sb env n (Hole t) = showb env "? " ". " n t

13631365 sb env n (GHole i t) = showb env "?defer " ". " n t

1366+ sb env n (Pi (Just _) t _) = showb env "{" "} -> " n t

13641367 sb env n (Pi _ t _) = showb env "(" ") -> " n t

13651368 sb env n (PVar t) = showb env "pat " ". " n t

13661369 sb env n (PVTy t) = showb env "pty " ". " n t

src/Idris/Core/Unify.hs+3−3

@@ -153,7 +153,7 @@ match_unify ctxt env topx topy inj holes from =

153153 h2 <- un bnames vx vy

154154 combine bnames h1 h2

155155 uB bnames (Lam tx) (Lam ty) = un bnames tx ty

156− uB bnames (Pi _ tx _) (Pi _ ty _) = un bnames tx ty

156+ uB bnames (Pi i tx _) (Pi i' ty _) = un bnames tx ty

157157 uB bnames x y = do UI s f <- get

158158 let r = recoverable (normalise ctxt env (binderTy x))

159159 (normalise ctxt env (binderTy y))

@@ -461,8 +461,8 @@ unify ctxt env topx topy inj holes usersupp from =

461461 h2 <- un' False (((x,y),binderTy bx):bnames) sx sy

462462 combine bnames h1 h2

463463 where sameBinder (Lam _) (Lam _) = True

464− sameBinder (Pi _ _ _) (Pi _ _ _) = True

465− sameBinder _ _ = False

464+ sameBinder (Pi i _ _) (Pi i' _ _) = True

465+ sameBinder _ _ = False -- never unify holes/guesses/etc

466466 un' fn bnames x y

467467 | OK True <- convEq' ctxt holes x y = do sc 1; return []

468468 | isUniverse x && isUniverse y = do sc 1; return []

src/Idris/DeepSeq.hs+1

@@ -202,6 +202,7 @@ instance NFData PTerm where

202202 rnf (PLet _ x1 x2 x3 x4)

203203 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

204204 rnf (PTyped x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205+ rnf (PAppImpl x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

205206 rnf (PApp x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

206207 rnf (PAppBind x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

207208 rnf (PMatchApp x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/ElabTerm.hs+83−37

@@ -164,13 +164,14 @@ getUnmatchable ctxt n | isDConName n ctxt && n /= inferCon

164164getUnmatchable ctxt n = []

165165

166166data ElabCtxt = ElabCtxt { e_inarg :: Bool,

167+ e_isfn :: Bool, -- ^ Function part of application

167168 e_guarded :: Bool,

168169 e_intype :: Bool,

169170 e_qq :: Bool,

170171 e_nomatching :: Bool -- ^ can't pattern match

171172 }

172173

173−initElabCtxt = ElabCtxt False False False False False

174+initElabCtxt = ElabCtxt False False False False False False

174175

175176goal_polymorphic :: ElabD Bool

176177goal_polymorphic =

@@ -244,7 +245,7 @@ elab ist info emode opts fn tm

244245 then solveAuto ist fn False a

245246 else return ()) as

246247

247− itm <- if not pattern then insertImpLam t else return t

248+ itm <- if not pattern then insertImpLam ina t else return t

248249 ct <- insertCoerce ina itm

249250 t' <- insertLazy ct

250251 g <- goal

@@ -596,17 +597,13 @@ elab ist info emode opts fn tm

596597 _ -> lift $ tfail (NoSuchVariable fn)

597598 ns <- match_apply (Var fn') (map (\x -> (x,0)) imps)

598599 solve

599− -- This isn't a sound way of checking for Typecase - we need a

600− -- better way!

601−-- elab' (_, _, inty, qq) (PApp fc (PRef _ f) args')

602−-- | isTConName f (tt_ctxt ist) && pattern && not reflection && not inty && not qq

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

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

605− elab' ina _ tm@(PApp fc (PRef _ f) args_in)

601+ -- FIXME: Anyone feel like refactoring this mess? - EB

602+ elab' ina topfc tm@(PApp fc (PRef _ f) args_in)

606603 | pattern && not reflection && e_nomatching ina

607604 = lift $ tfail $ Msg ("Attempting concrete match on polymorphic argument: " ++ show tm)

608− | otherwise

609− = do env <- get_env

605+ | otherwise = implicitApp $

606+ do env <- get_env

610607 ty <- goal

611608 fty <- get_type (Var f)

612609 ctxt <- get_context

@@ -614,18 +611,18 @@ elab ist info emode opts fn tm

614611 let unmatchableArgs = if pattern

615612 then getUnmatchable (tt_ctxt ist) f

616613 else []

617− -- Dot it if we're in a pattern and it isn't a constructor

618−-- when (pattern && not (isDConName f ctxt) && f /= fn) $ dotterm

619−

614+-- trace ("BEFORE " ++ show f ++ ": " ++ show ty) $

620615 when (pattern && not reflection && not (e_qq ina) && not (e_intype ina)

621616 && isTConName f (tt_ctxt ist)) $

622617 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

623618 if (f `elem` map fst env && length args == 1 && length args_in == 1)

624619 then -- simple app, as below

625− do simple_app False (elabE ina (Just fc) (PRef fc f))

620+ do simple_app False

621+ (elabE (ina { e_isfn = True }) (Just fc) (PRef fc f))

626622 (elabE (ina { e_inarg = True }) (Just fc) (getTm (head args)))

627623 (show tm)

628624 solve

625+ return []

629626 else

630627 do ivs <- get_instances

631628 ps <- get_probs

@@ -656,22 +653,58 @@ elab ist info emode opts fn tm

656653 (zip ns' (unmatchableArgs ++ repeat False))

657654 (f == sUN "Force")

658655 (map (\x -> getTm x) eargs) -- TODO: remove this False arg

659− solve

660− ivs' <- get_instances

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

662− -- i.e. no holes in them

663− when (not pattern || (e_inarg ina && not tcgen &&

664− not (e_guarded ina))) $

665− mapM_ (\n -> do focus n

666− g <- goal

667− env <- get_env

668− hs <- get_holes

669− if all (\n -> not (n `elem` hs)) (freeNames g)

670− then try (resolveTC False 7 g fn ist)

671− (movelast n)

672− else movelast n)

673− (ivs' \\ ivs)

674− where -- normal < alternatives < lambdas < rewrites < tactic < default tactic

656+ imp <- if (e_isfn ina) then

657+ do guess <- get_guess

658+ gty <- get_type (forget guess)

659+ env <- get_env

660+ let ty_n = normalise ctxt env gty

661+ return $ getReqImps ty_n

662+ else return []

663+ -- Now we find out how many implicits we needed at the

664+ -- end of the application by looking at the goal again

665+ -- - Have another go, but this time add the

666+ -- implicits (can't think of a better way than this...)

667+ case imp of

668+ rs@(_:_) | not pattern -> return rs -- quit, try again

669+ _ -> do solve

670+ hs <- get_holes

671+ ivs' <- get_instances

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

673+ -- i.e. no holes in them

674+ when (not pattern || (e_inarg ina && not tcgen &&

675+ not (e_guarded ina))) $

676+ mapM_ (\n -> do focus n

677+ g <- goal

678+ env <- get_env

679+ hs <- get_holes

680+ if all (\n -> not (n `elem` hs)) (freeNames g)

681+ then try (resolveTC False 7 g fn ist)

682+ (movelast n)

683+ else movelast n)

684+ (ivs' \\ ivs)

685+ return []

686+ where

687+ -- Run the elaborator, which returns how many implicit

688+ -- args were needed, then run it again with those args. We need

689+ -- this because we have to elaborate the whole application to

690+ -- find out whether any computations have caused more implicits

691+ -- to be needed.

692+ implicitApp :: ElabD [ImplicitInfo] -> ElabD ()

693+ implicitApp elab

694+ | pattern = do elab; return ()

695+ | otherwise

696+ = do s <- get

697+ imps <- elab

698+ case imps of

699+ [] -> return ()

700+ es -> do put s

701+ elab' ina topfc (PAppImpl tm es)

702+

703+ getReqImps (Bind x (Pi (Just i) ty _) sc)

704+ = i : getReqImps sc

705+ getReqImps _ = []

706+

707+ -- normal < alternatives < lambdas < rewrites < tactic < default tactic

675708 -- reason for lambdas after alternatives is that having

676709 -- the alternative resolved can help with typechecking the lambda

677710 -- or the rewrite. Rewrites/tactics need as much information

@@ -744,15 +777,24 @@ elab ist info emode opts fn tm

744777 setInjective (PApp _ (PRef _ n) _) = setinj n

745778 setInjective _ = return ()

746779

747− elab' ina _ tm@(PApp fc f [arg])

748− = erun fc $

780+ elab' ina _ tm@(PApp fc f [arg]) =

781+ erun fc $

749782 do simple_app (not $ headRef f)

750− (elabE ina (Just fc) f) (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

783+ (elabE (ina { e_isfn = True }) (Just fc) f)

784+ (elabE (ina { e_inarg = True }) (Just fc) (getTm arg))

751785 (show tm)

752786 solve

753787 where headRef (PRef _ _) = True

754788 headRef (PApp _ f _) = headRef f

755789 headRef _ = False

790+

791+ elab' ina fc (PAppImpl f es) = do appImpl (reverse es) -- not that we look...

792+ solve

793+ where appImpl [] = elab' (ina { e_isfn = False }) fc f -- e_isfn not set, so no recursive expansion of implicits

794+ appImpl (e : es) = simple_app False

795+ (appImpl es)

796+ (elab' ina fc Placeholder)

797+ (show f)

756798 elab' ina fc Placeholder

757799 = do (h : hs) <- get_holes

758800 movelast h

@@ -1072,16 +1114,20 @@ elab ist info emode opts fn tm

10721114 = x : insertScopedImps fc sc xs

10731115 insertScopedImps _ _ xs = xs

10741116

1075− insertImpLam t =

1117+ insertImpLam ina t =

10761118 do ty <- goal

10771119 env <- get_env

10781120 let ty' = normalise (tt_ctxt ist) env ty

10791121 addLam ty' t

10801122 where

10811123 -- just one level at a time

1082− addLam (Bind n (Pi (Just _) _ _) sc) t

1083− = do impn <- unique_hole (sMN 0 "imp")

1084− return (PLam emptyFC impn Placeholder t)

1124+ addLam (Bind n (Pi (Just _) _ _) sc) t =

1125+ do impn <- unique_hole (sMN 0 "imp")

1126+ if e_isfn ina -- apply to an implicit immediately

1127+ then return (PApp emptyFC

1128+ (PLam emptyFC impn Placeholder t)

1129+ [pexp Placeholder])

1130+ else return (PLam emptyFC impn Placeholder t)

10851131 addLam _ t = return t

10861132

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

src/Idris/IBC.hs+1

@@ -1482,6 +1482,7 @@ instance Binary PTerm where

14821482 PTyped x1 x2 -> do putWord8 7

14831483 put x1

14841484 put x2

1485+ PAppImpl x1 x2 -> error "PAppImpl in final term"

14851486 PApp x1 x2 x3 -> do putWord8 8

14861487 put x1

14871488 put x2

test/reg058/expectednew file

No changes to the content.

test/reg058/implicits.idrnew file+14

@@ -0,0 +1,14 @@

1+%default total

3+InterpBool : () -> Type

4+InterpBool () = {x : Type} -> x -> Nat

6+class IdrisBug (u : ()) where

7+ idrisBug : InterpBool u

9+instance IdrisBug () where

10+ idrisBug _ = Z

11+

12+f : Nat

13+f = idrisBug {u = ()} 'a'

14+

test/reg058/implicits2.idrnew file+19

@@ -0,0 +1,19 @@

1+import Data.Vect

3+impTy : Bool -> Type

4+impTy True = Int

5+impTy False = {n : Nat} -> Vect n Int -> Vect n Int

7+wibble : impTy False

8+wibble [] = []

9+wibble (x :: xs) = x * 2 :: wibble xs

10+

11+wobble : (b : Bool) -> impTy b

12+wobble True = 42

13+wobble False = wibble

14+

15+foo : Vect 4 Int

16+foo = wobble False [1,2,3,4]

17+

18+bar : Int

19+bar = wobble True

test/reg058/runnew file+5

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

1+#!/usr/bin/env bash

2+idris $@ implicits.idr --check

3+idris $@ implicits2.idr --check

5+rm -f *.ibc