Default superclass intances

This allows code like:

    data Identity i = Id i

    class Functor (f : Type -> Type) where
      map : (a -> b) -> f a -> f b

    class Functor f => Applicative (f : Type -> Type) where
      instance Functor f where
        map f fa = ap (pure f) fa
      pure : a -> f a
      ap : f (a -> b) -> f a -> f b

    instance Applicative Identity where
      pure = Id
      ap (Id f) (Id a) = Id (f a)

    data Nat = Z
             | S Nat

    x : Identity Nat
    x = map S (Id Z)

Note the default Functor instance defined as part of the Applicative
class. This allows the Identity data type to omit an explicit Functor
instance and one gets defined from the Applicative instance.

This feature is largely copied from the approach done in She:

https://personal.cis.strath.ac.uk/conor.mcbride/pub/she/superclass.html

It basically does macro expansion of each default superclass instance
(e.g. Functor) when the containing class (e.g. Applicative) gets an
instance defined. Currently, default superclass instance definitions
are not type-checked, only their macro expansions are.

Default superclass instances are limited to being defined for types
which are syntactically equal to one of the superclass constraints.

src/Core/Evaluate.hs

@@ -632,13 +632,6 @@ instance Show Def where
                                         show ns' ++ " " ++ show sc' ++ "\n\n" ++
             if inlc then "Inlinable\n" else "Not inlinable\n"
 
--- We need this for serialising Def. Fortunately, it never gets used because
--- we'll never serialise a primitive operator
-
-instance Binary (a -> b) where
-    put x = return ()
-    get = error "Getting a function"
-
 -------
 
 -- Frozen => doesn't reduce

src/Idris/AbsSyntax.hs

@@ -197,10 +197,10 @@ addInstance :: Bool -> Name -> Name -> Idris ()
 addInstance int n i
     = do ist <- getIState
          case lookupCtxt n (idris_classes ist) of
-                [CI a b c d ins] ->
-                     do let cs = addDef n (CI a b c d (addI i ins)) (idris_classes ist)
+                [CI a b c d e ins] ->
+                     do let cs = addDef n (CI a b c d e (addI i ins)) (idris_classes ist)
                         putIState $ ist { idris_classes = cs }
-                _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [i]) (idris_classes ist)
+                _ -> do let cs = addDef n (CI (MN 0 "none") [] [] [] [] [i]) (idris_classes ist)
                         putIState $ ist { idris_classes = cs }
   where addI i ins | int = i : ins
                    | chaser n = ins ++ [i]

src/Idris/AbsSyntaxTree.hs

@@ -748,6 +748,7 @@ type PArg = PArg' PTerm
 data ClassInfo = CI { instanceName :: Name,
                       class_methods :: [(Name, (FnOpts, PTerm))],
                       class_defaults :: [(Name, (Name, PDecl))], -- method name -> default impl
+                      class_default_superclasses :: [PDecl],
                       class_params :: [Name],
                       class_instances :: [Name] }
     deriving Show

src/Idris/DeepSeq.hs

@@ -320,9 +320,9 @@ instance (NFData t) => NFData (PArg' t) where
               rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
 
 instance NFData ClassInfo where
-        rnf (CI x1 x2 x3 x4 x5)
+        rnf (CI x1 x2 x3 x4 x5 x6)
           = rnf x1 `seq`
-              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()
+              rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()
 
 instance NFData OptInfo where
         rnf (Optimise x1 x2 x3 x4)

src/Idris/ElabDecls.hs

@@ -1541,6 +1541,8 @@ elabClass info syn doc fc constraints tn ps ds
                                   (map (pexp . PRef fc) (map fst ps))
          -- build data declaration
          let mdecls = filter tydecl ds -- method declarations
+         let idecls = filter instdecl ds -- default superclass instance declarations
+         mapM_ checkDefaultSuperclassInstance idecls
          let mnames = map getMName mdecls
          logLvl 2 $ "Building methods " ++ show mnames
          ims <- mapM (tdecl mnames) mdecls
@@ -1549,7 +1551,7 @@ elabClass info syn doc fc constraints tn ps ds
          let (methods, imethods)
               = unzip (map (\ ( x,y,z) -> (x, y)) ims)
          let defaults = map (\ (x, (y, z)) -> (x,y)) defs
-         addClass tn (CI cn (map nodoc imethods) defaults (map fst ps) [])
+         addClass tn (CI cn (map nodoc imethods) defaults idecls (map fst ps) [])
          -- build instance constructor type
          -- decorate names of functions to ensure they can't be referred
          -- to elsewhere in the class declaration
@@ -1571,7 +1573,6 @@ elabClass info syn doc fc constraints tn ps ds
          mapM_ (elabDecl EAll info) (concat fns)
          -- add the default definitions
          mapM_ (elabDecl EAll info) (concat (map (snd.snd) defs))
-         i <- getIState
          addIBC (IBCClass tn)
   where
     nodoc (n, (_, o, t)) = (n, (o, t))
@@ -1582,6 +1583,17 @@ elabClass info syn doc fc constraints tn ps ds
     mdec (NS x n) = NS (mdec x) n
     mdec x = x
 
+    -- TODO: probably should normalise
+    checkDefaultSuperclassInstance (PInstance _ fc cs n ps _ _ _)
+        = do when (not $ null cs) . tclift
+                $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))
+             i <- getIState
+             let t = PApp fc (PRef fc n) (map pexp ps)
+             let isConstrained = any (== t) constraints
+             when (not isConstrained) . tclift
+                $ tfail (At fc (Msg $ "Default instances must be for a superclass constraint on the containing class."))
+             return ()
+
     impbind [] x = x
     impbind ((n, ty): ns) x = PPi impl n ty (impbind ns x)
     conbind (ty : ns) x = PPi constraint (MN 0 "class") ty (conbind ns x)
@@ -1613,6 +1625,8 @@ elabClass info syn doc fc constraints tn ps ds
 
     tydecl (PTy _ _ _ _ _ _) = True
     tydecl _ = False
+    instdecl (PInstance _ _ _ _ _ _ _ _) = True
+    instdecl _ = False
     clause (PClauses _ _ _ _) = True
     clause _ = False
 
@@ -1698,15 +1712,12 @@ elabInstance info syn fc cs n ps t expn ds
                        [c] -> return c
                        _ -> ifail $ show fc ++ ":" ++ show n ++ " is not a type class"
          let constraint = PApp fc (PRef fc n) (map pexp ps)
-         let iname = case expn of
-                         Nothing -> SN (InstanceN n (map show ps))
-                          -- UN ('@':show n ++ "$" ++ show ps)
-                         Just nm -> nm
+         let iname = mkiname n ps expn
          nty <- elabType' True info syn "" fc [] iname t
          -- if the instance type matches any of the instances we have already,
          -- and it's not a named instance, then it's overlapping, so report an error
          case expn of
-            Nothing -> do mapM_ (checkNotOverlapping i (delab i nty)) 
+            Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping i (delab i nty))
                                 (class_instances ci)
                           addInstance intInst n iname
             Just _ -> addInstance intInst n iname
@@ -1720,6 +1731,9 @@ elabInstance info syn fc cs n ps t expn ds
                                   PApp _ _ args -> getWParams args
                                   _ -> return []) ps
          let pnames = map pname (concat (nub wparams))
+         let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)
+         undefinedSuperclassInstances <- filterM (fmap not . isOverlapping i) superclassInstances
+         mapM_ (elabDecl EAll info) undefinedSuperclassInstances
          let all_meths = map (nsroot . fst) (class_methods ci)
          let mtys = map (\ (n, (op, t)) ->
                    let t_in = substMatchesShadow ips pnames t 
@@ -1746,7 +1760,7 @@ elabInstance info syn fc cs n ps t expn ds
          let idecls = [PClauses fc [Dictionary] iname
                                  [PClause fc iname lhs [] rhs wb]]
          iLOG (show idecls)
-         mapM (elabDecl EAll info) idecls
+         mapM_ (elabDecl EAll info) idecls
          addIBC (IBCInstance intInst n iname)
 --          -- for each constraint, build a top level function to chase it
 --          logLvl 5 $ "Building functions"
@@ -1757,20 +1771,50 @@ elabInstance info syn fc cs n ps t expn ds
                 [PConstant (AType (ATInt ITNative))] -> True
                 _ -> False
 
-    checkNotOverlapping i t n
-     | take 2 (show n) == "@@" = return ()
+    mkiname n' ps' expn' =
+        case expn' of
+          Nothing -> SN (InstanceN n' (map show ps'))
+          Just nm -> nm
+
+    substInstance ips pnames (PInstance syn _ cs n ps t expn ds)
+        = PInstance syn fc cs n (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds
+
+    isOverlapping i (PInstance syn _ _ n ps t expn _)
+        = case lookupCtxtName n (idris_classes i) of
+            [(n, ci)] -> let iname = (mkiname n ps expn) in
+                            case lookupTy iname (tt_ctxt i) of
+                              [] -> elabFindOverlapping i ci iname syn t
+                              (_:_) -> return True
+            _ -> return False -- couldn't find class, just let elabInstance fail later
+
+    -- TODO: largely based upon elabType' - should try to abstract
+    elabFindOverlapping i ci iname syn t
+        = do ty' <- addUsingConstraints syn fc t
+             ty' <- implicit syn iname ty'
+             let ty = addImpl i ty'
+             ctxt <- getContext
+             ((tyT, _, _), _) <-
+                   tclift $ elaborate ctxt iname (TType (UVal 0)) []
+                            (errAt "type of " iname (erun fc (build i info False iname ty)))
+             ctxt <- getContext
+             (cty, _) <- recheckC fc [] tyT
+             let nty = normalise ctxt [] cty
+             return $ any (isJust . findOverlapping i (delab i nty)) (class_instances ci)
+
+    findOverlapping i t n
+     | take 2 (show n) == "@@" = Nothing
      | otherwise
         = case lookupTy n (tt_ctxt i) of
             [t'] -> let tret = getRetType t
                         tret' = getRetType (delab i t') in
                         case matchClause i tret' tret of
-                            Right ms -> overlapping tret tret'
+                            Right ms -> Just tret'
                             Left _ -> case matchClause i tret tret' of
-                                Right ms -> overlapping tret tret'
-                                Left _ -> return ()
-            _ -> return ()
-    overlapping t t' = tclift $ tfail (At fc (Msg $
-                            "Overlapping instance: " ++ show t' ++ " already defined"))
+                                Right ms -> Just tret'
+                                Left _ -> Nothing
+            _ -> Nothing
+    overlapping t' = tclift $ tfail (At fc (Msg $
+                          "Overlapping instance: " ++ show t' ++ " already defined"))
     getRetType (PPi _ _ _ sc) = getRetType sc
     getRetType t = t
 

src/Idris/ElabTerm.hs

@@ -641,7 +641,7 @@ findInstances :: IState -> Term -> [Name]
 findInstances ist t
     | (P _ n _, _) <- unApply t
         = case lookupCtxt n (idris_classes ist) of
-            [CI _ _ _ _ ins] -> ins
+            [CI _ _ _ _ _ ins] -> ins
             _ -> []
     | otherwise = []
 

src/Idris/IBC.hs

@@ -23,7 +23,7 @@ import Debug.Trace
 import Paths_idris
 
 ibcVersion :: Word8
-ibcVersion = 46
+ibcVersion = 47
 
 data IBCFile = IBCFile { ver :: Word8,
                          sourcefile :: FilePath,
@@ -225,7 +225,7 @@ pClasses cs = mapM_ (\ (n, c) ->
                            -- Don't lose instances from previous IBCs, which
                            -- could have loaded in any order
                            let is = case lookupCtxt n (idris_classes i) of
-                                      [CI _ _ _ _ ins] -> ins
+                                      [CI _ _ _ _ _ ins] -> ins
                                       _ -> []
                            let c' = c { class_instances =
                                           class_instances c ++ is }
@@ -807,10 +807,7 @@ instance Binary Def where
                    1 -> do x1 <- get
                            x2 <- get
                            return (TyDecl x1 x2)
-                   2 -> do x1 <- get
-                           x2 <- get
-                           x3 <- get
-                           return (Operator x1 x2 x3)
+                   -- Operator isn't written, don't read
                    3 -> do x1 <- get
                            x2 <- get
                            x3 <- get
@@ -1246,15 +1243,14 @@ instance Binary Using where
                     1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)
 
 instance Binary SyntaxInfo where
-        put (Syn x1 x2 x3 x4 x5 x6 x7 x8)
+        put (Syn x1 x2 x3 x4 _ x5 x6 x7)
           = do put x1
                put x2
                put x3
                put x4
                put x5
                put x6
                put x7
-               put x8
         get
           = do x1 <- get
                x2 <- get
@@ -1263,8 +1259,7 @@ instance Binary SyntaxInfo where
                x5 <- get
                x6 <- get
                x7 <- get
-               x8 <- get
-               return (Syn x1 x2 x3 x4 x5 x6 x7 x8)
+               return (Syn x1 x2 x3 x4 id x5 x6 x7)
 
 instance (Binary t) => Binary (PClause' t) where
         put x
@@ -1748,17 +1743,19 @@ instance (Binary t) => Binary (PArg' t) where
 
 
 instance Binary ClassInfo where
-        put (CI x1 x2 x3 x4 _)
+        put (CI x1 x2 x3 x4 x5 _)
           = do put x1
                put x2
                put x3
                put x4
+               put x5
         get
           = do x1 <- get
                x2 <- get
                x3 <- get
                x4 <- get
-               return (CI x1 x2 x3 x4 [])
+               x5 <- get
+               return (CI x1 x2 x3 x4 x5 [])
 
 instance Binary OptInfo where
         put (Optimise x1 x2 x3 x4)

src/Idris/Parser.hs

@@ -437,16 +437,35 @@ namespace syn =
        return [PNamespace n (concat ds)]
      <?> "namespace declaration"
 
-{- |Parses a methods block (for type classes and instances)
-  MethodsBlock ::= 'where' OpenBlock FnDecl* CloseBlock
+{- |Parses a methods block (for instances)
+  InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock
  -}
-methodsBlock :: SyntaxInfo -> IdrisParser [PDecl]
-methodsBlock syn = do reserved "where"
-                      openBlock
-                      ds <- many (fnDecl syn)
-                      closeBlock
-                      return (concat ds)
-                   <?> "methods block"
+instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]
+instanceBlock syn = do reserved "where"
+                       openBlock
+                       ds <- many (fnDecl syn)
+                       closeBlock
+                       return (concat ds)
+                    <?> "instance block"
+
+{- |Parses a methods and instances block (for type classes)
+
+MethodOrInstance ::=
+   FnDecl
+   | Instance
+   ;
+
+ClassBlock ::=
+  'where' OpenBlock MethodOrInstance* CloseBlock
+  ;
+-}
+classBlock :: SyntaxInfo -> IdrisParser [PDecl]
+classBlock syn = do reserved "where"
+                    openBlock
+                    ds <- many ((notEndBlock >> instance_ syn) <|> fnDecl syn)
+                    closeBlock
+                    return (concat ds)
+                 <?> "class block"
 
 {- |Parses a type class declaration
 
@@ -456,7 +475,7 @@ ClassArgument ::=
    ;
 
 Class ::=
-  DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* MethodsBlock?
+  DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?
   ;
 -}
 class_ :: SyntaxInfo -> IdrisParser [PDecl]
@@ -467,7 +486,7 @@ class_ syn = do (doc, acc) <- try (do
                 reserved "class"; fc <- getFC; cons <- constraintList syn; n_in <- name
                 let n = expandNS syn n_in
                 cs <- many carg
-                ds <- option [] (methodsBlock syn)
+                ds <- option [] (classBlock syn)
                 accData acc n (concatMap declared ds)
                 return [PClass doc syn fc cons n cs ds]
              <?> "type-class declaration"
@@ -481,7 +500,7 @@ class_ syn = do (doc, acc) <- try (do
 {- |Parses a type class instance declaration
 
   Instance ::=
-    'instance' InstanceName? ConstraintList? Name SimpleExpr* MethodsBlock?
+    'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?
     ;
 
   InstanceName ::= '[' Name ']';
@@ -494,9 +513,9 @@ instance_ syn = do reserved "instance"; fc <- getFC
                    args <- many (simpleExpr syn)
                    let sc = PApp fc (PRef fc cn) (map pexp args)
                    let t = bindList (PPi constraint) (map (\x -> (MN 0 "c", x)) cs) sc
-                   ds <- option [] (methodsBlock syn)
+                   ds <- option [] (instanceBlock syn)
                    return [PInstance syn fc cs cn args t en ds]
-                 <?> "instance declaratioN"
+                 <?> "instance declaration"
   where instanceName :: IdrisParser Name
         instanceName = do lchar '['; n_in <- fnName; lchar ']'
                           let n = expandNS syn n_in