@@ -1770,19 +1770,21 @@ elabClass info syn doc fc constraints tn ps ds
17701770 toExp ns e sc = sc
17711771
17721772elabInstance :: ElabInfo -> SyntaxInfo ->
1773+ ElabWhat -> -- phase
17731774 FC -> [PTerm] -> -- constraints
17741775 Name -> -- the class
17751776 [PTerm] -> -- class parameters (i.e. instance)
17761777 PTerm -> -- full instance type
17771778 Maybe Name -> -- explicit name
17781779 [PDecl] -> Idris ()
1779−elabInstance info syn fc cs n ps t expn ds
1780− = do i <- getIState
1781− (n, ci) <- case lookupCtxtName n (idris_classes i) of
1782− [c] -> return c
1783− _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1784− let constraint = PApp fc (PRef fc n) (map pexp ps)
1785− let iname = mkiname n ps expn
1780+elabInstance info syn what fc cs n ps t expn ds = do
1781+ i <- getIState
1782+ (n, ci) <- case lookupCtxtName n (idris_classes i) of
1783+ [c] -> return c
1784+ _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
1785+ let constraint = PApp fc (PRef fc n) (map pexp ps)
1786+ let iname = mkiname n ps expn
1787+ when (what /= EDefns) $ do
17861788 nty <- elabType' True info syn "" fc [] iname t
17871789 -- if the instance type matches any of the instances we have already,
17881790 -- and it's not a named instance, then it's overlapping, so report an error
@@ -1791,6 +1793,7 @@ elabInstance info syn fc cs n ps t expn ds
17911793 (class_instances ci)
17921794 addInstance intInst n iname
17931795 Just _ -> addInstance intInst n iname
1796+ when (what /= ETypes) $ do
17941797 let ips = zip (class_params ci) ps
17951798 let ns = case n of
17961799 NS n ns' -> ns'
@@ -2087,9 +2090,8 @@ elabDecl' what info (PClass doc s f cs n ps ds)
20872090 = do iLOG $ "Elaborating class " ++ show n
20882091 elabClass info (s { syn_params = [] }) doc f cs n ps ds
20892092elabDecl' what info (PInstance s f cs n ps t expn ds)
2090− | what /= ETypes
20912093 = do iLOG $ "Elaborating instance " ++ show n
2092− elabInstance info s f cs n ps t expn ds
2094+ elabInstance info s what f cs n ps t expn ds
20932095elabDecl' what info (PRecord doc s f tyn ty cdoc cn cty)
20942096 | what /= ETypes
20952097 = do iLOG $ "Elaborating record " ++ show tyn