@@ -33,6 +33,12 @@ import Data.List
3333import Data.Maybe
3434import Debug.Trace
3535
36+import qualified Data.Map as Map
37+import Data.Char(isLetter, toLower)
38+import Data.List.Split (splitOn)
39+
40+import Util.Pretty(pretty)
41+
3642recheckC fc env t
3743 = do -- t' <- applyOpts (forget t) (doesn't work, or speed things up...)
3844 ctxt <- getContext
@@ -143,9 +149,10 @@ elabPostulate info syn doc fc opts n ty
143149 -- remove it from the deferred definitions list
144150 solveDeferred n
145151
146−elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> Bool -> PData -> Idris ()
147−elabData info syn doc fc codata (PLaterdecl n t_in)
148− = do iLOG (show (fc, doc))
152+elabData :: ElabInfo -> SyntaxInfo -> String -> FC -> DataOpts -> PData -> Idris ()
153+elabData info syn doc fc opts (PLaterdecl n t_in)
154+ = do let codata = Codata `elem` opts
155+ iLOG (show (fc, doc))
149156 checkUndefined fc n
150157 ctxt <- getContext
151158 i <- getIState
@@ -161,8 +168,9 @@ elabData info syn doc fc codata (PLaterdecl n t_in)
161168 logLvl 2 $ "---> " ++ show cty
162169 updateContext (addTyDecl n (TCon 0 0) cty) -- temporary, to check cons
163170
164−elabData info syn doc fc codata (PDatadecl n t_in dcons)
165− = do iLOG (show fc)
171+elabData info syn doc fc opts (PDatadecl n t_in dcons)
172+ = do let codata = Codata `elem` opts
173+ iLOG (show fc)
166174 undef <- isUndefined fc n
167175 ctxt <- getContext
168176 i <- getIState
@@ -173,6 +181,9 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
173181 (errAt "data declaration " n (erun fc (build i info False n t)))
174182 def' <- checkDef fc defer
175183 let def'' = map (\(n, (i, top, t)) -> (n, (i, top, t, True))) def'
184+ -- if n is defined already, make sure it is just a type declaration
185+ -- with the same type we've just elaborated
186+ checkDefinedAs fc n t' (tt_ctxt i)
176187 addDeferredTyCon def''
177188 mapM_ (elabCaseBlock info []) is
178189 (cty, _) <- recheckC fc [] t'
@@ -194,7 +205,17 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
194205 collapseCons n cons
195206 updateContext (addDatatype (Data n ttag cty cons))
196207 mapM_ (checkPositive n) cons
208+ if DefaultEliminator `elem` opts then evalStateT (elabEliminator params n t dcons info) Map.empty
209+ else return ()
197210 where
211+ checkDefinedAs fc n t ctxt
212+ = case lookupDef n ctxt of
213+ [] -> return ()
214+ [TyDecl _ ty] ->
215+ case converts ctxt [] t ty of
216+ OK () -> return ()
217+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
218+ _ -> tclift $ tfail (At fc (AlreadyDefined n))
198219 -- parameters are names which are unchanged across the structure,
199220 -- which appear exactly once in the return type of a constructor
200221
@@ -245,12 +266,253 @@ elabData info syn doc fc codata (PDatadecl n t_in dcons)
245266 | otherwise = count n ts
246267 mParam args (_ : rest) = Nothing : mParam args rest
247268
269+type EliminatorState = StateT (Map.Map String Int) Idris
270+
271+-- TODO: Use uniqueName for generating names, rewrite everything to use idris_implicits instead of manual splitting, generally just rewrite
272+elabEliminator :: [Int] -> Name -> PTerm -> [(String, Name, PTerm, FC)] -> ElabInfo -> EliminatorState ()
273+elabEliminator paramPos n ty cons info = do
274+ elimLog $ "Elaborating eliminator"
275+ let (cnstrs, _) = splitPi ty
276+ let (splittedTy@(pms, idxs)) = splitPms cnstrs
277+ generalParams <- namePis False pms
278+ motiveIdxs <- namePis False idxs
279+ let motive = mkMotive n paramPos generalParams motiveIdxs
280+ consTerms <- mapM (\(c@(_,cnm,_,_)) -> do
281+ name <- freshName $ "elim_" ++ simpleName cnm
282+ consTerm <- extractConsTerm c generalParams
283+ return (name, expl, consTerm)) cons
284+ scrutineeIdxs <- namePis False idxs
285+ let motiveConstr = [(motiveName, expl, motive)]
286+ let scrutinee = (scrutineeName, expl, applyCons n (interlievePos paramPos generalParams scrutineeIdxs 0))
287+ let eliminatorTy = piConstr (generalParams ++ motiveConstr ++ consTerms ++ scrutineeIdxs ++ [scrutinee]) (applyMotive (map (\(n,_,_) -> PRef elimFC n) scrutineeIdxs) (PRef elimFC scrutineeName))
288+ let eliminatorTyDecl = PTy (show n) defaultSyntax elimFC [TotalFn] elimDeclName eliminatorTy
289+ let clauseConsElimArgs = map getPiName consTerms
290+ let clauseGeneralArgs' = map getPiName generalParams ++ [motiveName] ++ clauseConsElimArgs
291+ let clauseGeneralArgs = map (\arg -> pexp (PRef elimFC arg)) clauseGeneralArgs'
292+ let elimSig = "-- eliminator signature: " ++ showImp Nothing True True eliminatorTy
293+ eliminatorClauses <- mapM (\(cns, cnsElim) -> generateEliminatorClauses cns cnsElim clauseGeneralArgs generalParams) (zip cons clauseConsElimArgs)
294+ let eliminatorDef = PClauses emptyFC [TotalFn] elimDeclName eliminatorClauses
295+ elimLog $ "-- eliminator definition: " ++ showDeclImp True eliminatorDef
296+ Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorTyDecl) (\err -> return ())
297+ -- Do not elaborate clauses if there aren't any
298+ case eliminatorClauses of
299+ [] -> return ()
300+ _ -> Control.Monad.State.lift $ idrisCatch (elabDecl EAll info eliminatorDef) (\err -> return ())
301+ where elimLog :: String -> EliminatorState ()
302+ elimLog s = Control.Monad.State.lift (logLvl 2 s)
303+
304+ elimFC :: FC
305+ elimFC = fileFC "(eliminator)"
306+
307+ elimDeclName :: Name
308+ elimDeclName = SN $ ElimN n
309+
310+ applyNS :: Name -> [String] -> Name
311+ applyNS n [] = n
312+ applyNS n ns = NS n ns
313+
314+ splitPi :: PTerm -> ([(Name, Plicity, PTerm)], PTerm)
315+ splitPi = splitPi' []
316+ where splitPi' :: [(Name, Plicity, PTerm)] -> PTerm -> ([(Name, Plicity, PTerm)], PTerm)
317+ splitPi' acc (PPi pl n tyl tyr) = splitPi' ((n, pl, tyl):acc) tyr
318+ splitPi' acc t = (reverse acc, t)
319+
320+ splitPms :: [(Name, Plicity, PTerm)] -> ([(Name, Plicity, PTerm)], [(Name, Plicity, PTerm)])
321+ splitPms cnstrs = (map fst pms, map fst idxs)
322+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
323+
324+ isMachineGenerated :: Name -> Bool
325+ isMachineGenerated (MN _ _) = True
326+ isMachineGenerated _ = False
327+
328+ namePis :: Bool -> [(Name, Plicity, PTerm)] -> EliminatorState [(Name, Plicity, PTerm)]
329+ namePis keepOld pms = do names <- mapM (mkPiName keepOld) pms
330+ let oldNames = map fst names
331+ let params = map snd names
332+ return $ map (\(n, pl, ty) -> (n, pl, removeParamPis oldNames params ty)) params
333+
334+ mkPiName :: Bool -> (Name, Plicity, PTerm) -> EliminatorState (Name, (Name, Plicity, PTerm))
335+ mkPiName keepOld (n, pl, piarg) | not (isMachineGenerated n) && keepOld = do return (n, (n, pl, piarg))
336+ mkPiName _ (oldName, pl, piarg) = do name <- freshName $ keyOf piarg
337+ return (oldName, (name, pl, piarg))
338+ where keyOf :: PTerm -> String
339+ keyOf (PRef _ name) | isLetter (nameStart name) = (toLower $ nameStart name):"__"
340+ keyOf (PApp _ tyf _) = keyOf tyf
341+ keyOf PType = "ty__"
342+ keyOf _ = "carg__"
343+ nameStart :: Name -> Char
344+ nameStart n = nameStart' (simpleName n)
345+ where nameStart' :: String -> Char
346+ nameStart' "" = ' '
347+ nameStart' ns = head ns
348+
349+ simpleName :: Name -> String
350+ simpleName (NS n _) = simpleName n
351+ simpleName (MN i n) = n ++ show i
352+ simpleName n = show n
353+
354+ nameSpaces :: Name -> [String]
355+ nameSpaces (NS _ ns) = ns
356+ nameSpaces _ = []
357+
358+ freshName :: String -> EliminatorState Name
359+ freshName key = do
360+ nameMap <- get
361+ let i = fromMaybe 0 (Map.lookup key nameMap)
362+ let name = key ++ show i
363+ put $ Map.insert key (i+1) nameMap
364+ return (UN name)
365+
366+ scrutineeName :: Name
367+ scrutineeName = UN "scrutinee"
368+
369+ scrutineeArgName :: Name
370+ scrutineeArgName = UN "scrutineeArg"
371+
372+ motiveName :: Name
373+ motiveName = UN "prop"
374+
375+ mkMotive :: Name -> [Int] -> [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)] -> PTerm
376+ mkMotive n paramPos params indicies =
377+ let scrutineeTy = (scrutineeArgName, expl, applyCons n (interlievePos paramPos params indicies 0))
378+ in piConstr (indicies ++ [scrutineeTy]) PType
379+
380+ piConstr :: [(Name, Plicity, PTerm)] -> PTerm -> PTerm
381+ piConstr [] ty = ty
382+ piConstr ((n, pl, tyb):tyr) ty = PPi pl n tyb (piConstr tyr ty)
383+
384+ interlievePos :: [Int] -> [a] -> [a] -> Int -> [a]
385+ interlievePos idxs [] l2 i = l2
386+ interlievePos idxs l1 [] i = l1
387+ interlievePos idxs (x:xs) l2 i | i `elem` idxs = x:(interlievePos idxs xs l2 (i+1))
388+ interlievePos idxs l1 (y:ys) i = y:(interlievePos idxs l1 ys (i+1))
389+
390+ replaceParams :: [Int] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
391+ replaceParams paramPos params cns =
392+ let (_, cnsResTy) = splitPi cns
393+ in case cnsResTy of
394+ PApp _ _ args ->
395+ let oldParams = paramNamesOf 0 paramPos args
396+ in removeParamPis oldParams params cns
397+ _ -> cns
398+
399+ removeParamPis :: [Name] -> [(Name, Plicity, PTerm)] -> PTerm -> PTerm
400+ removeParamPis oldParams params (PPi pl n tyb tyr) =
401+ case findIndex (== n) oldParams of
402+ Nothing -> (PPi pl n (removeParamPis oldParams params tyb) (removeParamPis oldParams params tyr))
403+ Just i -> (removeParamPis oldParams params tyr)
404+ removeParamPis oldParams params (PRef _ n) =
405+ case findIndex (== n) oldParams of
406+ Nothing -> (PRef elimFC n)
407+ Just i -> let (newname,_,_) = params !! i in (PRef elimFC (newname))
408+ removeParamPis oldParams params (PApp _ cns args) =
409+ PApp elimFC (removeParamPis oldParams params cns) $ replaceParamArgs args
410+ where replaceParamArgs :: [PArg] -> [PArg]
411+ replaceParamArgs [] = []
412+ replaceParamArgs (arg:args) =
413+ case extractName (getTm arg) of
414+ [] -> arg:replaceParamArgs args
415+ [n] ->
416+ case findIndex (== n) oldParams of
417+ Nothing -> arg:replaceParamArgs args
418+ Just i -> let (newname,_,_) = params !! i in arg {getTm = PRef elimFC newname}:replaceParamArgs args
419+ removeParamPis oldParams params t = t
420+
421+ paramNamesOf :: Int -> [Int] -> [PArg] -> [Name]
422+ paramNamesOf i paramPos [] = []
423+ paramNamesOf i paramPos (arg:args) = (if i `elem` paramPos then extractName (getTm arg) else []) ++ paramNamesOf (i+1) paramPos args
424+
425+ extractName :: PTerm -> [Name]
426+ extractName (PRef _ n) = [n]
427+ extractName _ = []
428+
429+ splitArgPms :: PTerm -> ([PTerm], [PTerm])
430+ splitArgPms (PApp _ f args) = splitArgPms' args
431+ where splitArgPms' :: [PArg] -> ([PTerm], [PTerm])
432+ splitArgPms' cnstrs = (map (getTm . fst) pms, map (getTm . fst) idxs)
433+ where (pms, idxs) = partition (\c -> snd c `elem` paramPos) (zip cnstrs [0..])
434+ splitArgPms _ = ([],[])
435+
436+
437+ implicitIndexes :: (String, Name, PTerm, FC) -> EliminatorState [(Name, Plicity, PTerm)]
438+ implicitIndexes (cns@(doc, cnm, ty, fc)) = do
439+ i <- Control.Monad.State.lift getIState
440+ implargs' <- case lookupCtxt cnm (idris_implicits i) of
441+ [] -> do fail $ "Error while showing implicits for " ++ show cnm
442+ [args] -> do return args
443+ _ -> do fail $ "Ambigous name for " ++ show cnm
444+ let implargs = mapMaybe convertImplPi implargs'
445+ let (_, cnsResTy) = splitPi ty
446+ case cnsResTy of
447+ PApp _ _ args ->
448+ let oldParams = paramNamesOf 0 paramPos args
449+ in return $ filter (\(n,_,_) -> not (n `elem` oldParams))implargs
450+ _ -> return implargs
451+
452+ extractConsTerm :: (String, Name, PTerm, FC) -> [(Name, Plicity, PTerm)] -> EliminatorState PTerm
453+ extractConsTerm (doc, cnm, ty, fc) generalParameters = do
454+ let cons' = replaceParams paramPos generalParameters ty
455+ let (args, resTy) = splitPi cons'
456+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
457+ consArgs <- namePis True args
458+ let recArgs = findRecArgs consArgs
459+ let recMotives = map applyRecMotive recArgs
460+ let (_, consIdxs) = splitArgPms resTy
461+ return $ piConstr (implidxs ++ consArgs ++ recMotives) (applyMotive consIdxs (applyCons cnm consArgs))
462+ where applyRecMotive :: (Name, Plicity, PTerm) -> (Name, Plicity, PTerm)
463+ applyRecMotive (n,_,ty) = (UN $ "ih" ++ simpleName n, expl, applyMotive idxs (PRef elimFC n))
464+ where (_, idxs) = splitArgPms ty
465+
466+ findRecArgs :: [(Name, Plicity, PTerm)] -> [(Name, Plicity, PTerm)]
467+ findRecArgs [] = []
468+ findRecArgs (ty@(_,_,PRef _ tn):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
469+ findRecArgs (ty@(_,_,PApp _ (PRef _ tn) _):rs) | simpleName tn == simpleName n = ty:findRecArgs rs
470+ findRecArgs (ty:rs) = findRecArgs rs
471+
472+ applyCons :: Name -> [(Name, Plicity, PTerm)] -> PTerm
473+ applyCons tn targs = PApp elimFC (PRef elimFC tn) (map convertArg targs)
474+
475+ convertArg :: (Name, Plicity, PTerm) -> PArg
476+ convertArg (n, _, _) = pexp (PRef elimFC n)
477+
478+ applyMotive :: [PTerm] -> PTerm -> PTerm
479+ applyMotive idxs t = PApp elimFC (PRef elimFC motiveName) (map pexp idxs ++ [pexp t])
480+
481+ getPiName :: (Name, Plicity, PTerm) -> Name
482+ getPiName (name,_,_) = name
483+
484+ convertImplPi :: PArg -> Maybe (Name, Plicity, PTerm)
485+ convertImplPi (PImp {getTm = t, pname = n}) = Just (n, expl, t)
486+ convertImplPi _ = Nothing
487+
488+ generateEliminatorClauses :: (String, Name, PTerm, FC) -> Name -> [PArg] -> [(Name, Plicity, PTerm)] -> EliminatorState PClause
489+ generateEliminatorClauses (doc, cnm, ty, fc) cnsElim generalArgs generalParameters = do
490+ let cons' = replaceParams paramPos generalParameters ty
491+ let (args, resTy) = splitPi cons'
492+ i <- Control.Monad.State.lift getIState
493+ implidxs <- implicitIndexes (doc, cnm, ty, fc)
494+ let (_, generalIdxs') = splitArgPms resTy
495+ let generalIdxs = map pexp generalIdxs'
496+ consArgs <- namePis True args
497+ let lhsPattern = PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ generalIdxs ++ [pexp $ applyCons cnm consArgs])
498+ let recArgs = findRecArgs consArgs
499+ let recElims = map applyRecElim recArgs
500+ let rhsExpr = PApp elimFC (PRef elimFC cnsElim) (map convertArg implidxs ++ map convertArg consArgs ++ recElims)
501+ return $ PClause elimFC elimDeclName lhsPattern [] rhsExpr []
502+ where applyRecElim :: (Name, Plicity, PTerm) -> PArg
503+ applyRecElim (constr@(recCnm,_,recTy)) = pexp $ PApp elimFC (PRef elimFC elimDeclName) (generalArgs ++ map pexp idxs ++ [pexp $ PRef elimFC recCnm])
504+ where (_, idxs) = splitArgPms recTy
505+
248506-- | Elaborate primitives
249507
250508elabPrims :: Idris ()
251509elabPrims = do mapM_ (elabDecl EAll toplevel)
252− (map (PData "" defaultSyntax (fileFC "builtin") False)
253− [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl])
510+ (map (\(opt, decl) -> PData "" defaultSyntax (fileFC "builtin") opt decl)
511+ (zip
512+ [inferOpts, unitOpts, falseOpts, pairOpts, eqOpts]
513+ [inferDecl, unitDecl, falseDecl, pairDecl, eqDecl]))
514+ addNameHint eqTy (UN "prf")
515+ elabDecl EAll toplevel elimDecl
254516 mapM_ elabPrim primitives
255517 -- Special case prim__believe_me because it doesn't work on just constants
256518 elabBelieveMe
@@ -400,7 +662,7 @@ elabTransform info fc safe lhs_in rhs_in
400662elabRecord :: ElabInfo -> SyntaxInfo -> String -> FC -> Name ->
401663 PTerm -> String -> Name -> PTerm -> Idris ()
402664elabRecord info syn doc fc tyn ty cdoc cn cty
403− = do elabData info syn doc fc False (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
665+ = do elabData info syn doc fc [] (PDatadecl tyn ty [(cdoc, cn, cty, fc)])
404666 cty' <- implicit syn cn cty
405667 i <- getIState
406668 cty <- case lookupTy cn (tt_ctxt i) of
@@ -531,7 +793,7 @@ elabCon info syn tn codata (doc, n, t_in, fc)
531793 addIBC (IBCDef n)
532794 addDocStr n doc
533795 addIBC (IBCDoc n)
534− forceArgs n cty'
796+ forceArgs tn n cty'
535797 return (n, cty')
536798 where
537799 tyIs (Bind n b sc) = tyIs sc
@@ -638,7 +900,7 @@ elabClauses info fc opts n_in cs = let n = liftname info n_in in
638900 Just _ -> logLvl 5 $ "Partially evaluated:\n" ++ show pats
639901 _ -> return ()
640902
641− let optpdef = map debind optpats -- $ map (simple_lhs (tt_ctxt ist)) optpats
903+ let optpdef = map debind optpats -- \$ map (simple_lhs (tt_ctxt ist)) optpats
642904 tree@(CaseDef scargs sc _) <- tclift $
643905 simpleCase tcase False reflect CompileTime fc pdef
644906 cov <- coverage
@@ -797,7 +1059,7 @@ elabPE info fc caller r =
7971059
7981060 mkSpecialised ist specapp_in = do
7991061 let (specTy, specapp) = getSpecTy ist specapp_in
800− let (n, newnm, [(lhs, rhs)]) = getSpecClause ist specapp
1062+ let (n, newnm, pats) = getSpecClause ist specapp
8011063 let undef = case lookupDef newnm (tt_ctxt ist) of
8021064 [] -> True
8031065 _ -> False
@@ -812,10 +1074,12 @@ elabPE info fc caller r =
8121074 iLOG $ "PE definition type : " ++ (show specTy)
8131075 ++ "\n" ++ show opts
8141076 logLvl 2 $ "PE definition " ++ show newnm ++ ":\n" ++
815− (showImp Nothing True False lhs ++ " = " ++
816− showImp Nothing True False rhs)
1077+ showSep "\n"
1078+ (map (\ (lhs, rhs) ->
1079+ (showImp Nothing True False lhs ++ " = " ++
1080+ showImp Nothing True False rhs)) pats)
8171081 elabType info defaultSyntax "" fc opts newnm specTy
818− let def = [PClause fc newnm lhs [] rhs []]
1082+ let def = map (\ (lhs, rhs) -> PClause fc newnm lhs [] rhs []) pats
8191083 elabClauses info fc opts newnm def
8201084 logLvl 1 $ "Specialised " ++ show newnm)
8211085 -- if it doesn't work, just don't specialise. Could happen for lots
@@ -918,7 +1182,18 @@ checkPossible info fc tcgen fname lhs_in
9181182-- b <- inferredDiff fc (delab' i lhs_tm True) lhs
9191183-- return (not b) -- then return (Just lhs_tm) else return Nothing
9201184-- trace (show (delab' i lhs_tm True) ++ "\n" ++ show lhs) $ return (not b)
921− err@(Error _) -> return False
1185+ Error err -> return (impossibleError err)
1186+ where impossibleError (CantUnify _ topx topy e _ _)
1187+ = not (sameFam topx topy || not (impossibleError e))
1188+ impossibleError (CantConvert _ _ _) = False
1189+ impossibleError (At _ e) = impossibleError e
1190+ impossibleError (Elaborating _ _ e) = impossibleError e
1191+ impossibleError _ = True
1192+
1193+ sameFam topx topy
1194+ = case (unApply topx, unApply topy) of
1195+ ((P _ x _, _), (P _ y _, _)) -> x == y
1196+ _ -> False
9221197
9231198elabClause :: ElabInfo -> FnOpts -> (Int, PClause) ->
9241199 Idris (Either Term (Term, Term))
@@ -926,7 +1201,8 @@ elabClause info opts (_, PClause fc fname lhs_in [] PImpossible [])
9261201 = do let tcgen = Dictionary `elem` opts
9271202 b <- checkPossible info fc tcgen fname lhs_in
9281203 case b of
929− True -> ifail $ show fc ++ ":" ++ show lhs_in ++ " is a possible case"
1204+ True -> tclift $ tfail (At fc
1205+ (Msg $ show lhs_in ++ " is a valid case"))
9301206 False -> do ptm <- mkPatTm lhs_in
9311207 return (Left ptm)
9321208elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)
@@ -1268,6 +1544,8 @@ elabClass info syn doc fc constraints tn ps ds
12681544 (map (pexp . PRef fc) (map fst ps))
12691545 -- build data declaration
12701546 let mdecls = filter tydecl ds -- method declarations
1547+ let idecls = filter instdecl ds -- default superclass instance declarations
1548+ mapM_ checkDefaultSuperclassInstance idecls
12711549 let mnames = map getMName mdecls
12721550 logLvl 2 $ "Building methods " ++ show mnames
12731551 ims <- mapM (tdecl mnames) mdecls
@@ -1276,7 +1554,7 @@ elabClass info syn doc fc constraints tn ps ds
12761554 let (methods, imethods)
12771555 = unzip (map (\ ( x,y,z) -> (x, y)) ims)
12781556 let defaults = map (\ (x, (y, z)) -> (x,y)) defs
1279− addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])
1557+ addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])
12801558 -- build instance constructor type
12811559 -- decorate names of functions to ensure they can't be referred
12821560 -- to elsewhere in the class declaration
@@ -1286,7 +1564,7 @@ elabClass info syn doc fc constraints tn ps ds
12861564 let cons = [("", cn, cty, fc)]
12871565 let ddecl = PDatadecl tn tty cons
12881566 logLvl 5 $ "Class data " ++ showDImp True ddecl
1289− elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc False ddecl
1567+ elabData info (syn { no_imp = no_imp syn ++ mnames }) doc fc [] ddecl
12901568 -- for each constraint, build a top level function to chase it
12911569 logLvl 5 $ "Building functions"
12921570 let usyn = syn { using = map (\ (x,y) -> UImplicit x y) ps
@@ -1298,7 +1576,6 @@ elabClass info syn doc fc constraints tn ps ds
12981576 mapM_ (elabDecl EAll info) (concat fns)
12991577 -- add the default definitions
13001578 mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
1301− i <- getIState
13021579 addIBC (IBCClass tn)
13031580 where
13041581 nodoc (n, (_, o, t)) = (n, (o, t))
@@ -1309,6 +1586,17 @@ elabClass info syn doc fc constraints tn ps ds
13091586 mdec (NS x n) = NS (mdec x) n
13101587 mdec x = x
13111588
1589+ -- TODO: probably should normalise
1590+ checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)
1591+ = do when (not $ null cs) . tclift
1592+ $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))
1593+ i <- getIState
1594+ let t = PApp fc (PRef fc n) (map pexp ps)
1595+ let isConstrained = any (== t) constraints
1596+ when (not isConstrained) . tclift
1597+ $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
1598+ return ()
1599+
13121600 impbind [] x = x
13131601 impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
13141602 conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
@@ -1340,6 +1628,8 @@ elabClass info syn doc fc constraints tn ps ds
13401628
13411629 tydecl (PTy _ _ _ _ _ _) = True
13421630 tydecl _ = False
1631+ instdecl (PInstance _ _ _ _ _ _ _ _) = True
1632+ instdecl _ = False
13431633 clause (PClauses _ _ _ _) = True
13441634 clause _ = False
13451635
@@ -1425,15 +1715,12 @@ elabInstance info syn fc cs n ps t expn ds
14251715 [c] -> return c
14261716 _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
14271717 let constraint = PApp fc (PRef fc n) (map pexp ps)
1428− let iname = case expn of
1429− Nothing -> SN (InstanceN n (map show ps))
1430− -- UN ('@':show n ++ "$" ++ show ps)
1431− Just nm -> nm
1718+ let iname = mkiname n ps expn
14321719 nty <- elabType' True info syn "" fc [] iname t
14331720 -- if the instance type matches any of the instances we have already,
14341721 -- and it's not a named instance, then it's overlapping, so report an error
14351722 case expn of
1436− Nothing -> do mapM_ (checkNotOverlapping i (delab i nty))
1723+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
14371724 (class_instances ci)
14381725 addInstance intInst n iname
14391726 Just _ -> addInstance intInst n iname
@@ -1447,6 +1734,9 @@ elabInstance info syn fc cs n ps t expn ds
14471734 PApp _ _ args -> getWParams args
14481735 _ -> return []) ps
14491736 let pnames = map pname (concat (nub wparams))
1737+ let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
1738+ undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
1739+ mapM_ (elabDecl EAll info) undefinedSuperclassInstances
14501740 let all_meths = map (nsroot . fst) (class_methods ci)
14511741 let mtys = map (\ (n, (op, t)) ->
14521742 let t_in = substMatchesShadow ips pnames t
@@ -1473,7 +1763,7 @@ elabInstance info syn fc cs n ps t expn ds
14731763 let idecls = [PClauses fc [Dictionary] iname
14741764 [PClause fc iname lhs [] rhs wb]]
14751765 iLOG (show idecls)
1476− mapM (elabDecl EAll info) idecls
1766+ mapM_ (elabDecl EAll info) idecls
14771767 addIBC (IBCInstance intInst n iname)
14781768-- -- for each constraint, build a top level function to chase it
14791769-- logLvl 5 $ "Building functions"
@@ -1484,20 +1774,50 @@ elabInstance info syn fc cs n ps t expn ds
14841774 [PConstant (AType (ATInt ITNative))] -> True
14851775 _ -> False
14861776
1487− checkNotOverlapping i t n
1488− | take 2 (show n) == "@@" = return ()
1777+ mkiname n' ps' expn' =
1778+ case expn' of
1779+ Nothing -> SN (InstanceN n' (map show ps'))
1780+ Just nm -> nm
1781+
1782+ substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
1783+ = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
1784+
1785+ isOverlapping i (PInstance syn _ _ n ps t expn _)
1786+ = case lookupCtxtName n (idris_classes i) of
1787+ [(n, ci)] -> let iname = (mkiname n ps expn) in
1788+ case lookupTy iname (tt_ctxt i) of
1789+ [] -> elabFindOverlapping i ci iname syn t
1790+ (_:_) -> return True
1791+ _ -> return False -- couldn't find class, just let elabInstance fail later
1792+
1793+ -- TODO: largely based upon elabType' - should try to abstract
1794+ elabFindOverlapping i ci iname syn t
1795+ = do ty' <- addUsingConstraints syn fc t
1796+ ty' <- implicit syn iname ty'
1797+ let ty = addImpl i ty'
1798+ ctxt <- getContext
1799+ ((tyT, _, _), _) <-
1800+ tclift $ elaborate ctxt iname (TType (UVal 0)) []
1801+ (errAt "type of " iname (erun fc (build i info False iname ty)))
1802+ ctxt <- getContext
1803+ (cty, _) <- recheckC fc [] tyT
1804+ let nty = normalise ctxt [] cty
1805+ return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
1806+
1807+ findOverlapping i t n
1808+ | take 2 (show n) == "@@" = Nothing
14891809 | otherwise
14901810 = case lookupTy n (tt_ctxt i) of
14911811 [t'] -> let tret = getRetType t
14921812 tret' = getRetType (delab i t') in
14931813 case matchClause i tret' tret of
1494− Right ms -> overlapping tret tret'
1814+ Right ms -> Just tret'
14951815 Left _ -> case matchClause i tret tret' of
1496− Right ms -> overlapping tret tret'
1497− Left _ -> return ()
1498− _ -> return ()
1499− overlapping t t' = tclift $ tfail (At fc (Msg $
1500− "Overlapping instance: " ++ show t' ++ " already defined"))
1816+ Right ms -> Just tret'
1817+ Left _ -> Nothing
1818+ _ -> Nothing
1819+ overlapping t' = tclift $ tfail (At fc (Msg $
1820+ "Overlapping instance: " ++ show t' ++ " already defined"))
15011821 getRetType (PPi _ _ _ sc) = getRetType sc
15021822 getRetType t = t
15031823
@@ -1709,7 +2029,7 @@ elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
17092029 elabRecord info s doc f tyn ty cdoc cn cty
17102030 | otherwise
17112031 = do iLOG $ "Elaborating [type of] " ++ show tyn
1712− elabData info s doc f False (PLaterdecl tyn ty)
2032+ elabData info s doc f [] (PLaterdecl tyn ty)
17132033elabDecl' _ info (PDSL n dsl)
17142034 = do i <- getIState
17152035 putIState (i { idris_dsls = addDef n dsl (idris_dsls i) })