15737d9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Trickiness with implicits in dependent classes

Need to expand implicits for methods in the dictionary declarataion, but not quite the same way as for the top level function of the same name (i.e. need to leave out the dictionary itself). Fixes #1975

commit15737d9c4bf0f9e485d207170a68c5eb5374cede authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 19 Mar 2015, 12:56 (12 years ago) parent2a2468f

16 files changed+72−44

compare with master

unifiedsplit

idris.cabal+3 src/Idris/AbsSyntax.hs+28−18 src/Idris/AbsSyntaxTree.hs+4−1 src/Idris/Coverage.hs+1−1 src/Idris/DeepSeq.hs+2−2 src/Idris/Elab/Class.hs+11−11 src/Idris/Elab/Clause.hs+1−1 src/Idris/Elab/Data.hs+2−1 src/Idris/Elab/Instance.hs+1−1 src/Idris/Elab/Type.hs+4−4 src/Idris/Elab/Value.hs+1−1 src/Idris/IBC.hs+2−2 src/Idris/TypeSearch.hs+1−1 test/reg059/expected test/reg059/reg059.idr+8 test/reg059/run+3

idris.cabal+3

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

289289 test/reg058/run

290290 test/reg058/*.idr

291291 test/reg058/expected

292+ test/reg059/run

293+ test/reg059/*.idr

294+ test/reg059/expected

292295

293296 test/basic001/run

294297 test/basic001/*.idr

src/Idris/AbsSyntax.hs+28−18

@@ -1481,31 +1481,34 @@ implicitise syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

14811481

14821482-- Add implicit arguments in function calls

14831483addImplPat :: IState -> PTerm -> PTerm

1484−addImplPat = addImpl' True [] []

1484+addImplPat = addImpl' True [] [] []

14851485

14861486addImplBound :: IState -> [Name] -> PTerm -> PTerm

1487−addImplBound ist ns = addImpl' False ns [] ist

1487+addImplBound ist ns = addImpl' False ns [] [] ist

14881488

14891489addImplBoundInf :: IState -> [Name] -> [Name] -> PTerm -> PTerm

1490−addImplBoundInf ist ns inf = addImpl' False ns inf ist

1490+addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

14911491

14921492-- | Add the implicit arguments to applications in the term

1493−addImpl :: IState -> PTerm -> PTerm

1493+-- [Name] gives the names to always expend, even when under a binder of

1494+-- that name (this is to expand methods with implicit arguments in dependent

1495+-- type classes).

1496+addImpl :: [Name] -> IState -> PTerm -> PTerm

14941497addImpl = addImpl' False [] []

14951498

14961499-- TODO: in patterns, don't add implicits to function names guarded by constructors

14971500-- and *not* inside a PHidden

14981501

1499−addImpl' :: Bool -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1500−addImpl' inpat env infns ist ptm

1502+addImpl' :: Bool -> [Name] -> [Name] -> [Name] -> IState -> PTerm -> PTerm

1503+addImpl' inpat env infns imp_meths ist ptm

15011504 = mkUniqueNames env (ai False (zip env (repeat Nothing)) [] ptm)

15021505 where

15031506 ai :: Bool -> [(Name, Maybe PTerm)] -> [[T.Text]] -> PTerm -> PTerm

15041507 ai qq env ds (PRef fc f)

15051508 | f `elem` infns = PInferRef fc f

1506− | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq ist fc f ds []

1509+ | not (f `elem` map fst env) = handleErr $ aiFn inpat inpat qq imp_meths ist fc f ds []

15071510 ai qq env ds (PHidden (PRef fc f))

1508− | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq ist fc f ds [])

1511+ | not (f `elem` map fst env) = PHidden (handleErr $ aiFn inpat False qq imp_meths ist fc f ds [])

15091512 ai qq env ds (PEq fc lt rt l r)

15101513 = let lt' = ai qq env ds lt

15111514 rt' = ai qq env ds rt

@@ -1541,7 +1544,7 @@ addImpl' inpat env infns ist ptm

15411544 | f `elem` infns = ai qq env ds (PApp fc (PInferRef fc f) as)

15421545 | not (f `elem` map fst env)

15431546 = let as' = map (fmap (ai qq env ds)) as in

1544− handleErr $ aiFn inpat False qq ist fc f ds as'

1547+ handleErr $ aiFn inpat False qq imp_meths ist fc f ds as'

15451548 | Just (Just ty) <- lookup f env =

15461549 let as' = map (fmap (ai qq env ds)) as

15471550 arity = getPArity ty in

@@ -1576,7 +1579,9 @@ addImpl' inpat env infns ist ptm

15761579 _ -> ai qq env ds (PCase fc val [(PRef fc n, sc)])

15771580 ai qq env ds (PPi p n ty sc)

15781581 = let ty' = ai qq env ds ty

1579− sc' = ai qq ((n, Just ty):env) ds sc in

1582+ env' = if n `elem` imp_meths then env

1583+ else ((n, Just ty) : env)

1584+ sc' = ai qq env' ds sc in

15801585 PPi p n ty' sc'

15811586 ai qq env ds (PGoal fc r n sc)

15821587 = let r' = ai qq env ds r

@@ -1600,8 +1605,8 @@ addImpl' inpat env infns ist ptm

16001605-- if in a pattern, and there are no arguments, and there's no possible

16011606-- names with zero explicit arguments, don't add implicits.

16021607

1603−aiFn :: Bool -> Bool -> Bool -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1604−aiFn inpat True qq ist fc f ds []

1608+aiFn :: Bool -> Bool -> Bool -> [Name] -> IState -> FC -> Name -> [[T.Text]] -> [PArg] -> Either Err PTerm

1609+aiFn inpat True qq imp_meths ist fc f ds []

16051610 = case lookupDef f (tt_ctxt ist) of

16061611 [] -> Right $ PPatvar fc f

16071612 alts -> let ialts = lookupCtxtName f (idris_implicits ist) in

@@ -1609,7 +1614,7 @@ aiFn inpat True qq ist fc f ds []

16091614 if (not (vname f) || tcname f

16101615 || any (conCaf (tt_ctxt ist)) ialts)

16111616-- any constructor alts || any allImp ialts))

1612− then aiFn inpat False qq ist fc f ds [] -- use it as a constructor

1617+ then aiFn inpat False qq imp_meths ist fc f ds [] -- use it as a constructor

16131618 else Right $ PPatvar fc f

16141619 where imp (PExp _ _ _ _) = False

16151620 imp _ = True

@@ -1623,9 +1628,9 @@ aiFn inpat True qq ist fc f ds []

16231628 vname (UN n) = True -- non qualified

16241629 vname _ = False

16251630

1626−aiFn inpat expat qq ist fc f ds as

1631+aiFn inpat expat qq imp_meths ist fc f ds as

16271632 | f `elem` primNames = Right $ PApp fc (PRef fc f) as

1628−aiFn inpat expat qq ist fc f ds as

1633+aiFn inpat expat qq imp_meths ist fc f ds as

16291634 -- This is where namespaces get resolved by adding PAlternative

16301635 = do let ns = lookupCtxtName f (idris_implicits ist)

16311636 let nh = filter (\(n, _) -> notHidden n) ns

@@ -1633,15 +1638,20 @@ aiFn inpat expat qq ist fc f ds as

16331638 [] -> nh

16341639 x -> x

16351640 case ns' of

1636− [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)

1641+ [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc (isImpName f f')) (insertImpl ns as)

16371642 [] -> if f `elem` (map fst (idris_metavars ist))

16381643 then Right $ PApp fc (PRef fc f) as

16391644 else Right $ mkPApp fc (length as) (PRef fc f) as

16401645 alts -> Right $

16411646 PAlternative True $

1642− map (\(f', ns) -> mkPApp fc (length ns) (PRef fc f')

1647+ map (\(f', ns) -> mkPApp fc (length ns) (PRef fc (isImpName f f'))

16431648 (insertImpl ns as)) alts

16441649 where

1650+ -- if the name is in imp_meths, we should actually refer to the bound

1651+ -- name rather than the global one after expanding implicits

1652+ isImpName f f' | f `elem` imp_meths = f

1653+ | otherwise = f'

1654+

16451655 trimAlts [] alts = alts

16461656 trimAlts ns alts

16471657 = filter (\(x, _) -> any (\d -> d `isPrefixOf` nspace x) ns) alts

@@ -1685,7 +1695,7 @@ aiFn inpat expat qq ist fc f ds as

16851695 PImp p True l n Placeholder :

16861696 insImpAcc (M.insert n Placeholder pnas) ps given imps

16871697 insImpAcc pnas (PTacImplicit p l n sc' ty : ps) given imps =

1688− let sc = addImpl ist (substMatches (M.toList pnas) sc') in

1698+ let sc = addImpl imp_meths ist (substMatches (M.toList pnas) sc') in

16891699 case find n imps [] of

16901700 Just (tm, imps') ->

16911701 PTacImplicit p l n sc tm :

src/Idris/AbsSyntaxTree.hs+4−1

@@ -1198,6 +1198,9 @@ data SyntaxInfo = Syn { using :: [Using],

11981198 syn_params :: [(Name, PTerm)],

11991199 syn_namespace :: [String],

12001200 no_imp :: [Name],

1201+ imp_methods :: [Name], -- class methods. When expanding

1202+ -- implicits, these should be expanded even under

1203+ -- binders

12011204 decoration :: Name -> Name,

12021205 inPattern :: Bool,

12031206 implicitAllowed :: Bool,

@@ -1211,7 +1214,7 @@ deriving instance NFData SyntaxInfo

12111214deriving instance Binary SyntaxInfo

12121215!-}

12131216

1214−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL 0

1217+defaultSyntax = Syn [] [] [] [] [] id False False Nothing 0 initDSL 0

12151218

12161219expandNS :: SyntaxInfo -> Name -> Name

12171220expandNS syn n@(NS _ _) = n

src/Idris/Coverage.hs+1−1

@@ -24,7 +24,7 @@ import Control.Monad.State.Strict

2424-- provided explicitly from new clause generation.

2525mkPatTm :: PTerm -> Idris Term

2626mkPatTm t = do i <- getIState

27− let timp = addImpl' True [] [] i t

27+ let timp = addImpl' True [] [] [] i t

2828 evalStateT (toTT (mapPT deNS timp)) 0

2929 where

3030 toTT (PRef _ n) = do i <- lift getIState

src/Idris/DeepSeq.hs+2−2

@@ -353,10 +353,10 @@ instance NFData Using where

353353 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

354354

355355instance NFData SyntaxInfo where

356− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

356+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

357357 = rnf x1 `seq`

358358 rnf x2 `seq`

359359 rnf x3 `seq`

360360 rnf x4 `seq`

361361 rnf x5 `seq`

362− rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

362+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` ()

src/Idris/Elab/Class.hs+11−11

@@ -77,28 +77,28 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

7777 = unzip (map (\ ( x,y,z) -> (x, y)) ims)

7878 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

7979 -- build instance constructor type

80− -- decorate names of functions to ensure they can't be referred

81− -- to elsewhere in the class declaration

8280 let cty = impbind ps $ conbind constraints

8381 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

8482 constraint

8583 let cons = [(emptyDocstring, [], cn, cty, fc, [])]

8684 let ddecl = PDatadecl tn tty cons

8785 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

88− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc pDocs fc [] ddecl

89−

86+ -- Elaborate the data declaration

87+ elabData info (syn { no_imp = no_imp syn ++ mnames,

88+ imp_methods = mnames }) doc pDocs fc [] ddecl

9089 dets <- findDets cn fds

9190 addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [] dets)

91+

9292 -- for each constraint, build a top level function to chase it

93− logLvl 5 $ "Building functions"

94−-- let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps

95−-- ++ using syn }

96− fns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

97− mapM_ (rec_elabDecl info EAll info) (concat fns)

93+ cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

94+ mapM_ (rec_elabDecl info EAll info) (concat cfns)

95+

9896 -- for each method, build a top level function

9997 fns <- mapM (tfun cn constraint syn (map fst imethods)) imethods

10098 logLvl 5 $ "Functions " ++ show fns

99+ -- Elaborate the the top level methods

101100 mapM_ (rec_elabDecl info EAll info) (concat fns)

101+

102102 -- add the default definitions

103103 mapM_ (rec_elabDecl info EAll info) (concat (map (snd.snd) defs))

104104 addIBC (IBCClass tn)

@@ -134,8 +134,8 @@ elabClass info syn_in doc fc constraints tn ps pDocs fds ds

134134

135135 getMName (PTy _ _ _ _ _ n _) = nsroot n

136136 tdecl allmeths (PTy doc _ syn _ o n t)

137− = do t' <- implicit' info syn allmeths n t

138− logLvl 5 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

137+ = do t' <- implicit' info syn (map fst ps ++ allmeths) n t

138+ logLvl 2 $ "Method " ++ show n ++ " : " ++ showTmImpls t'

139139 return ( (n, (toExp (map fst ps) Exp t')),

140140 (n, (doc, o, (toExp (map fst ps)

141141 (\ l s p -> Imp l s p Nothing) t'))),

src/Idris/Elab/Clause.hs+1−1

@@ -548,7 +548,7 @@ elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->

548548elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])

549549 = do let tcgen = Dictionary `elem` opts

550550 i <- get

551− let lhs = addImpl i lhs_in

551+ let lhs = addImpl [] i lhs_in

552552 b <- checkPossible info fc tcgen fname lhs_in

553553 case b of

554554 True -> tclift $ tfail (At fc

src/Idris/Elab/Data.hs+2−1

@@ -215,6 +215,7 @@ elabCon :: ElabInfo -> SyntaxInfo -> Name -> Bool ->

215215 Idris (Name, Type)

216216elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

217217 = do checkUndefined fc n

218+ logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t_in

218219 (cty, ckind, t, inacc) <- buildType info syn fc [Constructor] n (if codata then mkLazy t_in else t_in)

219220 ctxt <- getContext

220221 let cty' = normalise ctxt [] cty

@@ -223,7 +224,7 @@ elabCon info syn tn codata expkind (doc, argDocs, n, t_in, fc, forcenames)

223224 -- Check that the constructor type is, in fact, a part of the family being defined

224225 tyIs n cty'

225226

226− logLvl 2 $ show fc ++ ":Constructor " ++ show n ++ " : " ++ show t

227+ logLvl 5 $ show fc ++ ":Constructor " ++ show n ++ " elaborated : " ++ show t

227228 logLvl 5 $ "Inaccessible args: " ++ show inacc

228229 logLvl 2 $ "---> " ++ show n ++ " : " ++ show cty'

229230

src/Idris/Elab/Instance.hs+1−1

@@ -167,7 +167,7 @@ elabInstance info syn doc argDocs what fc cs n ps t expn ds = do

167167 = do ty' <- addUsingConstraints syn fc t

168168 -- TODO think: something more in info?

169169 ty' <- implicit info syn iname ty'

170− let ty = addImpl i ty'

170+ let ty = addImpl [] i ty'

171171 ctxt <- getContext

172172 (ElabResult tyT _ _ ctxt' newDecls, _) <-

173173 tclift $ elaborate ctxt iname (TType (UVal 0)) initEState

src/Idris/Elab/Type.hs+4−4

@@ -57,13 +57,13 @@ buildType info syn fc opts n ty' = do

5757 ctxt <- getContext

5858 i <- getIState

5959

60− logLvl 3 $ show n ++ " pre-type " ++ showTmImpls ty'

60+ logLvl 2 $ show n ++ " pre-type " ++ showTmImpls ty' ++ show (no_imp syn)

6161 ty' <- addUsingConstraints syn fc ty'

6262 ty' <- addUsingImpls syn n fc ty'

63− let ty = addImpl i ty'

63+ let ty = addImpl (imp_methods syn) i ty'

6464

65− logLvl 3 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66− logLvl 3 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

65+ logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

66+ logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

6767

6868 (ElabResult tyT' defer is ctxt' newDecls, log) <-

6969 tclift $ elaborate ctxt n (TType (UVal 0)) initEState

src/Idris/Elab/Value.hs+1−1

@@ -56,7 +56,7 @@ elabValBind :: ElabInfo -> ElabMode -> Bool -> PTerm -> Idris (Term, Type, [(Nam

5656elabValBind info aspat norm tm_in

5757 = do ctxt <- getContext

5858 i <- getIState

59− let tm = addImpl i tm_in

59+ let tm = addImpl [] i tm_in

6060 logLvl 10 (showTmImpls tm)

6161 -- try:

6262 -- * ordinary elaboration

src/Idris/IBC.hs+2−2

@@ -1420,7 +1420,7 @@ instance Binary Using where

14201420 _ -> error "Corrupted binary data for Using"

14211421

14221422instance Binary SyntaxInfo where

1423− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

1423+ put (Syn x1 x2 x3 x4 _ _ x5 x6 _ _ x7 _)

14241424 = do put x1

14251425 put x2

14261426 put x3

@@ -1436,7 +1436,7 @@ instance Binary SyntaxInfo where

14361436 x5 <- get

14371437 x6 <- get

14381438 x7 <- get

1439− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 0)

1439+ return (Syn x1 x2 x3 x4 [] id x5 x6 Nothing 0 x7 0)

14401440

14411441instance (Binary t) => Binary (PClause' t) where

14421442 put x

src/Idris/TypeSearch.hs+1−1

@@ -46,7 +46,7 @@ searchByType pkgs pterm = do

4646 mapM_ loadPkgIndex pkgs

4747 pterm' <- addUsingConstraints syn emptyFC pterm

4848 pterm'' <- implicit toplevel syn name pterm'

49− let pterm''' = addImpl i pterm''

49+ let pterm''' = addImpl [] i pterm''

5050 ty <- elabType toplevel syn (fst noDocs) (snd noDocs) emptyFC [] name pterm'

5151 let names = searchUsing searchPred i ty

5252 let names' = take numLimit names

test/reg059/expectednew file

No changes to the content.

test/reg059/reg059.idrnew file+8

@@ -0,0 +1,8 @@

1+class Monad m => ContainerMonad (m : Type -> Type) where

2+ Elem : a -> m a -> Type

3+ tagElem : (mx : m a) -> m (x : a ** Elem x mx)

5+class Monad m => ContainerMonad2 a (m : Type -> Type) where

6+ Elem2 : a -> m a -> Type

7+ tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

test/reg059/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg059.idr --check

3+rm -f *.ibc