9d295be · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix dictionary arguments in dependent type class methods

Type class methods references were previously elaborated using the ordinary function call elaboration, but their class isn't yet available when the method lookup function is elaborated. This leads to a "can't resolve type class" error on the type class definition. Now, they have an explicit dictionary argument inserted, pointing at the dictionary that's used for the type of the method whose signature they appear in. Fixes #2302.

commit9d295be047b840120255610b0af44efe200bce84 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateWed 20 May 2015, 11:23 (11 years ago) parent5a366ac

5 files changed+76−16

compare with master

unifiedsplit

idris.cabal+3 src/Idris/Elab/Class.hs+44−16 test/reg065/expected test/reg065/reg065.idr+26 test/reg065/run+3

idris.cabal+3

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

314314 test/reg064/run

315315 test/reg064/*.idr

316316 test/reg064/expected

317+ test/reg065/run

318+ test/reg065/*.idr

319+ test/reg065/expected

317320

318321 test/basic001/run

319322 test/basic001/*.idr

src/Idris/Elab/Class.hs+44−16

@@ -1,4 +1,5 @@

11{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-missing-signatures #-}

23module Idris.Elab.Class(elabClass) where

45import Idris.AbsSyntax

@@ -47,6 +48,7 @@ import qualified Data.Set as S

4748import qualified Data.Text as T

4849import Data.Char(isLetter, toLower)

4950import Data.List.Split (splitOn)

51+import Data.Generics.Uniplate.Data (transform)

5052

5153import Util.Pretty(pretty, text)

5254

@@ -83,6 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

8385 let (methods, imethods)

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

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

88+

8689 -- build instance constructor type

8790 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

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

@@ -92,6 +95,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

9295 let ddecl = PDatadecl tn NoFC tty cons

9396

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

98+

9599 -- Elaborate the data declaration

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

97101 imp_methods = mnames }) doc pDocs fc [] ddecl

@@ -118,7 +122,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

118122 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

119123 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

120124 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

121−

125+

122126 where

123127 nodoc (n, (_, _, o, t)) = (n, (o, t))

124128

@@ -132,11 +136,6 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

132136 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t

133137 chkUniq _ t = t

134138

135− mdec :: Name -> Name

136− mdec (UN n) = SN (MethodN (UN n))

137− mdec (NS x n) = NS (mdec x) n

138− mdec x = x

139−

140139 -- TODO: probably should normalise

141140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

142141 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)

@@ -171,7 +170,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

171170 defdecl mtys c d@(PClauses fc opts n cs) =

172171 case lookup n mtys of

173172 Just (nfc, syn, o, ty) ->

174− do let ty' = insertConstraint c ty

173+ do let ty' = insertConstraint c (map fst mtys) ty

175174 let ds = map (decorateid defaultdec)

176175 [PTy emptyDocstring [] syn fc [] n nfc ty',

177176 PClauses fc (o ++ opts) n cs]

@@ -215,10 +214,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

215214 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

216215 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

217216

218− -- Generate a top level function which looks up a method in a given

217+ -- | Generate a top level function which looks up a method in a given

219218 -- dictionary (this is inlinable, always)

219+ tfun :: Name -- ^ The name of the class

220+ -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

221+ -> SyntaxInfo -> [Name] -- ^ All the method names

222+ -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))

223+ -- ^ The present declaration

224+ -> Idris [PDecl]

220225 tfun cn c syn all (m, (mfc, doc, o, ty))

221− = do let ty' = expandMethNS syn (insertConstraint c ty)

226+ = do let ty' = expandMethNS syn (insertConstraint c all ty)

222227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

223228 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

224229 let margs = getMArgs ty

@@ -236,6 +241,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

236241 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc

237242 getMArgs _ = []

238243

244+ getMeth :: [Name] -> [Name] -> Name -> PTerm

239245 getMeth (m:ms) (a:as) x | x == a = PRef fc m

240246 | otherwise = getMeth ms as x

241247

@@ -249,10 +255,24 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

249255 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

250256 rhsArgs [] _ = []

251257

252− insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)

253− = PPi p n fc ty (insertConstraint c sc)

254− insertConstraint c sc = PPi (constraint { pstatic = Static })

255− (sMN 0 "class") NoFC c sc

258+ insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

259+ insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)

260+ = PPi p n fc ty (insertConstraint c all sc)

261+ insertConstraint c all sc = let dictN = sMN 0 "class"

262+ in PPi (constraint { pstatic = Static })

263+ dictN NoFC c

264+ (constrainMeths (map basename all)

265+ dictN sc)

266+ where

267+ -- After we insert the constraint into the lookup, we need to

268+ -- ensure that the same dictionary is used to resolve lookups

269+ -- to the other methods in the class

270+ constrainMeths :: [Name] -> Name -> PTerm -> PTerm

271+ constrainMeths allM dictN tm = transform (addC allM dictN) tm

272+ addC allM dictN m@(PRef fc n)

273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC dictN)]

274+ | otherwise = m

275+ addC _ _ tm = tm

256276

257277 -- make arguments explicit and don't bind class parameters

258278 toExp ns e (PPi (Imp l s p _) n fc ty sc)

@@ -261,6 +281,13 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

261281 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

262282 toExp ns e sc = sc

263283

284+-- | Get the method declaration name corresponding to a user-provided name

285+mdec :: Name -> Name

286+mdec (UN n) = SN (MethodN (UN n))

287+mdec (NS x n) = NS (mdec x) n

288+mdec x = x

289+

290+-- | Get the docstring corresponding to a member, if one exists

264291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

265292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

266293memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

@@ -270,17 +297,18 @@ memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

270297memberDocs _ = Nothing

271298

272299

273−-- In a top level type for a method, expand all the method names namespaces

300+-- | In a top level type for a method, expand all the method names' namespaces

274301-- so that we don't have to disambiguate later

275−expandMethNS :: SyntaxInfo

302+expandMethNS :: SyntaxInfo

276303 -> PTerm -> PTerm

277304expandMethNS syn = mapPT expand

278305 where

279306 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

280307 expand t = t

281308

309+-- | Find the determining parameter locations

282310findDets :: Name -> [Name] -> Idris [Int]

283−findDets n ns =

311+findDets n ns =

284312 do i <- getIState

285313 return $ case lookupTyExact n (tt_ctxt i) of

286314 Just ty -> getDetPos 0 ns ty

test/reg065/expectednew file

No changes to the content.

test/reg065/reg065.idrnew file+26

@@ -0,0 +1,26 @@

1+||| Test that dependent type class definitions work.

2+|||

3+||| Fixes a regression where previous methods used in a later method's

4+||| type would lead to "can't resolve type class" errors

5+module TypeClassDep

7+import Data.Vect

10+class Foo a where

11+ getLen : Nat

12+ item : a -> Vect getLen a

13+

14+instance Foo () where

15+ getLen = 3

16+ item () = [(), (), ()]

17+

18+instance Foo String where

19+ getLen = 1

20+ item str = [str]

21+

22+check1 : item () = with Vect [(),(),()]

23+check1 = Refl

24+

25+check2 : item "halløjsa" = with Vect ["halløjsa"]

26+check2 = Refl

test/reg065/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ reg065.idr --check

3+rm -f *.ibc