Automatic derivation of instances

makefile

@@ -309,6 +309,7 @@ quine-tests: $(quine-test-targets)
 
 file-check-tests: just-build
 	misc/file-check tests/instance-interface-syntax-tests.dx $(dex) -O script
+	misc/file-check tests/deriving-instance-tests.dx $(dex) -O script
 
 run-%: export DEX_ALLOW_CONTRACTIONS=0
 run-%: export DEX_TEST_MODE=t

src/lib/AbstractSyntax.hs

@@ -134,6 +134,7 @@ topDecl = dropSrc topDecl' where
       return (fromString methodName, ty')
     return $ UInterface params' methodTys (fromString name) (toNest methodNames)
   topDecl' (CInstanceDecl def) = aInstanceDef def
+  topDecl' (CDerivingDecl def) = aDerivingDef def
   topDecl' (CEffectDecl _ _) = error "not implemented"
   topDecl' (CHandlerDecl _ _ _ _ _ _) = error "not implemented"
 
@@ -165,6 +166,13 @@ aInstanceDef (CInstanceDef clName args givens methods instNameAndParams) = do
           return $ UInstance clName' (catUOptAnnExplBinders givens' params') args' methods' instName' ExplicitApp
         Nothing -> return $ UInstance clName' givens' args' methods' instName' ImplicitApp
 
+aDerivingDef :: CDerivingDef -> SyntaxM (UTopDecl VoidS VoidS)
+aDerivingDef (CDerivingDef clName args givens) = do
+  let clName' = fromString clName
+  args' <- mapM expr args
+  givens' <- aOptGivens givens
+  return $ UDerivingInstance clName' givens' args'
+
 aDef :: CDef -> SyntaxM (SourceName, ULamExpr VoidS)
 aDef (CDef name params optRhs optGivens body) = do
   explicitParams <- aExplicitParams params

src/lib/ConcreteSyntax.hs

@@ -199,6 +199,7 @@ topDecl' =
   <|> interfaceDef
   <|> (CInstanceDecl <$> instanceDef True)
   <|> (CInstanceDecl <$> instanceDef False)
+  <|> (CDerivingDecl <$> derivingDef)
   <|> effectDef
 
 proseBlock :: Parser SourceBlock'
@@ -377,6 +378,15 @@ instanceDef isNamed = do
   methods <- withIndent $ withSrc cDecl `sepBy1` try nextLine
   return $ CInstanceDef className args givens methods optNameAndArgs
 
+derivingDef :: Parser CDerivingDef
+derivingDef = do
+  keyWord DerivingKW
+  keyWord InstanceKW
+  className <- anyName
+  args <- argList
+  givens <- optional givenClause
+  return $ CDerivingDef className args givens
+
 funDefLet :: Parser CDef
 funDefLet = label "function definition" do
   keyWord DefKW

src/lib/Inference.hs

@@ -126,6 +126,106 @@ inferTopUDecl (UInstance className instanceBs params methods maybeName expl) res
       instanceAtomName <- emitTopLet (getNameHint instanceName') PlainLet $ Atom lam
       applyRename (instanceName' @> atomVarName instanceAtomName) result
     _ -> error "impossible"
+inferTopUDecl (UDerivingInstance className instanceBs params) result = do
+  let (InternalName _ _ className') = className
+  -- Extract the following:
+  --   1) type parameter (`newTy`) for this instance,
+  --   2) the underlying type (`wrappedTy`) that is wrapped by `newTy`,
+  --   3) superclasses and method definitions from the instance definition for
+  --      `wrappedTy`.
+  --      (Note that in order to find the instance definition for `wrappedTy`
+  --      and instance dictionary for `wrappedTy` is synthesized first.)
+  -- All of 1-3 are valid under the binders `instanceBs`. Hence we create an
+  -- abstraction whose body contains 1), 2), and 3).
+  ab :: Abs (Nest (WithRoleExpl CBinder))
+            (CType `PairE` CType `PairE` (ListE CAtom) `PairE` (ListE CAtom))
+            n
+    <- liftInfererM $ solveLocal do
+      withRoleUBinders instanceBs do
+        ClassDef classSourceName _ _ roleExpls paramBinders _ _ <- lookupClassDef (sink className')
+        let expls = snd <$> roleExpls
+        params' <- checkInstanceParams expls paramBinders params
+        case params' of
+          [param] -> do
+            case param of
+              TypeAsAtom newTy@(NewtypeTyCon (UserADTType _ tcName (TyConParams _ tcParams))) -> do
+                tcDef <- lookupTyCon tcName
+                case tcDef of
+                  TyConDef _ _ conBs (ADTCons [DataConDef _ (EmptyAbs (Nest (_:>wrappedTy) Empty)) _ _]) -> do
+                    wrappedTy' <- applySubst (conBs @@> map SubstVal tcParams) wrappedTy
+                    let wrappedDictTy = DictType classSourceName (sink className') [TypeAsAtom wrappedTy']
+                    -- Synthesize the dictionary for `wrappedTy'`
+                    synthWrappedDict <- trySynthTerm (DictTy wrappedDictTy) Full
+                    -- Extract superclasses and methods from the synthesized dictionary for `wrappedTy'`:
+                    DictCon _ (InstanceDict wrappedInstName wrappedInstParams) <- return synthWrappedDict
+                    InstanceDef _ _ wrappedBinders _ body <- lookupInstanceDef wrappedInstName
+                    InstanceBody scs methods <- applySubst (wrappedBinders @@> map SubstVal wrappedInstParams) body
+                    return $ newTy `PairE` wrappedTy' `PairE` (ListE scs) `PairE` (ListE methods)
+                  TyConDef _ _ _ _ ->
+                    throw TypeErr $ "User-defined ADT " ++ pprint newTy ++
+                                    " does not have exactly one (data) constructor" ++
+                                    " that takes exactly one (data) argument"
+              _ -> throw TypeErr $ "Parameter " ++ pprint param ++ " not a user-defined ADT"
+          _ -> throw TypeErr $ "More than one parameter when deriving instance of class " ++ pprint className ++
+                              "\nparameters: " ++ pprint params'
+  -- Check that the class method types mention neither `newTy` nor `wrappedTy`.
+  -- There is no fundamental reason for disallowing occurrences of `newTy` or
+  -- `wrappedTy` in the class method types, but the current implementation of
+  -- `convertAtom` necessitates that neither `newTy` nor `wrappedTy` appears in
+  -- any of the class method types. The function `convertAtom` is used below to
+  -- synthesize instance methods for `newTy`, and this synthesis is guided by
+  -- occurrences of `newTy` and `wrappedTy` in the _instance_ method types of
+  -- `wrappedTy`. For `convertAtom` to work correctly, the types `newTy` and
+  -- `wrappedTy` may only occur in the _instance_ method types in those positions
+  -- where `clParamBinders` (defined by a pattern match below) occur in the
+  -- corresponding _class_ method types.
+  -- (Note that at this point, `clParamBinders` necessarily  consists of exactly
+  -- one binder, corresponding to `param` that has been scrutinized in the nested
+  -- `case` expressions above.)
+  liftExceptEnvReaderM $ refreshAbs ab \_ body -> do
+    let newTy `PairE` wrappedTy `PairE` _ `PairE` _ = body
+    ClassDef _ methodNames _ _ clParamBinders clScs methodTys <- lookupClassDef (sink className')
+    refreshAbs (concatAbs (Abs clParamBinders (Abs clScs (ListE methodTys)))) \_ (ListE methodTys') ->
+      foldM (\_ (mty, mname) -> do whenM (corePiTypeMentionsType mty (sink wrappedTy))
+                                         (throw TypeErr $ "Cannot derive instance of " ++ pprint className' ++ ": " ++
+                                                          "interface method `" ++ pprint mname ++ "` has type `" ++
+                                                          pprint mty ++ "`, which mentions the wrapped instance type `" ++
+                                                          pprint wrappedTy ++ "`")
+                                   whenM (corePiTypeMentionsType mty (sink newTy))
+                                         (throw TypeErr $ "Cannot derive instance of " ++ pprint className' ++ ": " ++
+                                                          "interface method `" ++ pprint mname ++ "` has type `" ++
+                                                          pprint mty ++ "`, which mentions the new instance type `" ++
+                                                          pprint newTy ++ "`")
+                                   return ())
+            ()
+            (zip methodTys' methodNames)
+  -- Finally, synthesize an instance definition for `newTy`. This requires, in
+  -- particular, that instance method definitions are synthesized for `newTy`.
+  -- The function `convertAtom` is used below to synthesize method definitions for
+  -- `newTy` from the corresponding instance methods for `wrappedTy` (the definitions
+  -- of which are held in the variable `methods` that is bound by a pattern match
+  -- on `body` below). In order to call `convertAtom`, an isomorphism (variable
+  -- `iso` below) between the types `newTy` and `wrappedTy` is first set up below.
+  def <- liftEnvReaderM $ refreshAbs ab \bs body -> do
+    let newTy `PairE` wrappedTy `PairE` ListE scs `PairE` ListE methods = body
+    case newTy of
+      NewtypeTyCon (UserADTType sName tcName tcParams) -> do
+        -- Forward isomorphism:
+        fwdAbs <- buildAbs noHint wrappedTy \x ->
+          return $ NewtypeCon (sink $ UserADTData sName tcName tcParams) (Var x)
+        -- Backward isomorphism:
+        bwdAbs <- buildAbs noHint newTy \x ->
+          return $ ProjectElt (sink newTy) UnwrapNewtype (Var x)
+        -- Bundled up isomorphisms:
+        let iso = Iso wrappedTy newTy fwdAbs bwdAbs
+        -- Convert methods with the constructed isomorphism between `wrappedTy'` and `newTy'`:
+        methods' <- liftBuilder $ mapM (convertAtom iso) methods
+        let (roleExpls, bs') = unzipAttrs bs
+        return $ InstanceDef className' roleExpls bs' [TypeAsAtom newTy] $ InstanceBody scs methods'
+      _ -> error "internal error"
+  instanceName <- emitInstanceDef def
+  addInstanceSynthCandidate className' instanceName
+  UDeclResultDone <$> return result
 inferTopUDecl (ULocalDecl (WithSrcB src decl)) result = addSrcContext src case decl of
   UPass -> return $ UDeclResultDone result
   UExprDecl _ -> error "Shouldn't have this at the top level (should have become a command instead)"
@@ -161,6 +261,121 @@ getInstanceType (InstanceDef className roleExpls bs params _) = liftEnvReaderM d
     let dTy = DictTy $ DictType classSourceName className' params'
     return $ CorePiType ImplicitApp (snd <$> roleExpls) bs' $ EffTy Pure dTy
 
+absMentionsType :: (EnvReader m, ScopeReader m) => Abs (Nest CBinder) CType n -> CType n -> m n Bool
+absMentionsType (Abs Empty scrut) ty = typeMentionsType scrut ty
+absMentionsType (Abs (Nest b@(_ :> bty) rest) scrut) ty = do
+  btyMentions <- typeMentionsType bty ty
+  restMentions <- liftEnvReaderM $ refreshAbs (Abs b (Abs rest scrut)) \_ ab -> absMentionsType ab (sink ty)
+  return $ btyMentions || restMentions
+
+corePiTypeMentionsType :: (EnvReader m, ScopeReader m) => CorePiType n -> CType n -> m n Bool
+corePiTypeMentionsType (CorePiType _ _ bs (EffTy _ scrut)) ty = absMentionsType (Abs bs scrut) ty
+
+typeMentionsType :: (EnvReader m, ScopeReader m) => CType n -> CType n -> m n Bool
+typeMentionsType scrutinee ty = do
+  isAlphaEq <- alphaEq scrutinee ty
+  if isAlphaEq then return True
+  else case scrutinee of
+    TC (BaseType _) -> return False
+    TC (ProdType scruts) -> anyM (flip typeMentionsType $ ty) scruts
+    TC (SumType scruts) -> anyM (flip typeMentionsType $ ty) scruts
+    TC (RefType _ scrut) -> typeMentionsType scrut ty
+    TC TypeKind -> return False
+    TC HeapType -> return False
+    TabPi (TabPiType _ b scrut) -> absMentionsType (Abs (Nest b Empty) scrut) ty
+    DepPairTy (DepPairType _ b scrut) -> absMentionsType (Abs (Nest b Empty) scrut) ty
+    TyVar _ -> return False
+    DictTy _ -> return False
+    Pi corePiType -> corePiTypeMentionsType corePiType ty
+    NewtypeTyCon _ -> return False
+    ProjectEltTy scrut _ _ -> typeMentionsType scrut ty
+
+data Iso n = Iso { inType :: CType n
+                 , outType :: CType n
+                 , fwd :: Abs CBinder CAtom n  -- single-argument abstraction that implements forward isomorphism
+                 , bwd :: Abs CBinder CAtom n  -- single-argument abstraction that implements backward isomorphism
+                 }
+
+instance GenericE Iso where
+  type RepE Iso = (CType `PairE` CType `PairE` (Abs CBinder CAtom) `PairE` (Abs CBinder CAtom))
+  fromE (Iso inType outType fwd bwd) = inType `PairE` outType `PairE` fwd `PairE` bwd
+  {-# INLINE fromE #-}
+  toE (inType `PairE` outType `PairE` fwd `PairE` bwd) = Iso inType outType fwd bwd
+  {-# INLINE toE #-}
+
+instance HoistableE Iso
+instance SinkableE Iso
+instance RenameE Iso
+
+instance Show (Iso n) where
+  show (Iso inType outType _ _) = "Iso " ++ pprint inType ++ " -> " ++ pprint outType
+
+instance Pretty (Iso n) where
+  pretty (Iso inType outType fwd bwd) = "Iso" <+> pretty inType <+> pretty outType <+>
+                                                  pretty (show fwd) <+> pretty (show bwd)
+
+invert :: Iso n -> Iso n
+invert iso = Iso inType' outType' fwd' bwd'
+  where inType' = outType iso
+        outType' = inType iso
+        fwd' = bwd iso
+        bwd' = fwd iso
+
+convertType :: EnvExtender m
+             => Iso o -> CType o -> m o (CType o)
+convertType iso ty = do
+  isTyEqualToInType <- alphaEq (inType iso) ty
+  if isTyEqualToInType then return $ outType iso
+  else case ty of
+    Pi (CorePiType appExpl expls bs (EffTy effs resultTy)) -> do
+      (Abs bs' (effs' `PairE` resultTy')) <- convertBinders iso (Abs (zipAttrs expls bs) (effs `PairE` resultTy))
+      let (_, bs'') = unzipAttrs bs'
+      return $ Pi $ CorePiType appExpl expls bs'' (EffTy effs' resultTy')
+    _ -> return ty
+
+convertBinders :: EnvExtender m
+               => Iso o
+               -> Abs (Nest (WithExpl CBinder)) (EffectRow 'CoreIR `PairE` CType) o
+               -> m o (Abs (Nest (WithExpl CBinder)) (EffectRow 'CoreIR `PairE` CType) o)
+convertBinders iso (Abs Empty (eff `PairE` ty)) = do
+  ty' <- convertType iso ty
+  return $ Abs Empty (eff `PairE` ty')
+convertBinders iso (Abs (Nest (WithAttrB expl (b:>bTy)) rest) x) = do
+  bTy' <- convertType iso bTy
+  refreshAbs (Abs (WithAttrB expl (b:>bTy')) (Abs rest x))
+    \(WithAttrB expl' (b':>bTy'')) ab -> do
+      Abs rest' x' <- convertBinders (sink iso) ab
+      return $ Abs (Nest (WithAttrB expl' (b':>bTy'')) rest') x'
+
+convertAtom :: (EnvExtender m, ScopableBuilder CoreIR m)
+         => Iso i
+         -> CAtom i ->  m i (CAtom i)
+convertAtom iso atom = do
+  let ty = getType atom
+  isTyEqualToInType <- alphaEq (inType iso) ty
+  if isTyEqualToInType
+    then applyAbs (fwd iso) (SubstVal atom)
+    else case ty of
+      Pi (CorePiType appExpl expl bs (EffTy effs bodyTy)) -> case atom of
+        Lam (CoreLamExpr _ _) -> do
+          Abs bs' (effs' `PairE` bodyTy') <- convertBinders iso (Abs (zipAttrs expl bs) (effs `PairE` bodyTy))
+          let (_, bs'') = unzipAttrs bs'
+          lamExpr <- buildCoreLam (CorePiType appExpl expl bs'' (EffTy effs' bodyTy')) \binderNames -> do
+            let args = map Var binderNames
+            args' <- mapM (convertAtom (sink $ invert iso)) args
+            -- Note that `App atom args'` (two lines down) has the unconverted
+            -- type `bodyTy` (and unconverted effects `effs`). After the recursive
+            -- call to `convertMethodAtom` (three lines down), the resulting
+            -- `atom''` will have the correct converted type and effects (i.e.
+            -- type and effects equivalent to `bodyTy'` and `effs'`).
+            effTy <- applyRename (bs @@> (map atomVarName binderNames)) $ EffTy effs bodyTy
+            atom' <- emitExpr $ App effTy (sink atom) args'
+            atom'' <- convertAtom (sink iso) atom'
+            emitExpr $ Atom atom''
+          return $ Lam lamExpr
+        _ -> error "should not occur"
+      _ -> return atom
+
 -- === Inferer interface ===
 
 class ( MonadFail1 m, Fallible1 m, Catchable1 m, CtxReader1 m, Builder CoreIR m )

src/lib/Lexing.hs

@@ -80,7 +80,7 @@ checkNotKeyword p = try $ do
 
 data KeyWord = DefKW | ForKW | For_KW | RofKW | Rof_KW | CaseKW | OfKW
              | DataKW | StructKW | InterfaceKW
-             | InstanceKW | GivenKW | WithKW | SatisfyingKW
+             | InstanceKW | GivenKW | WithKW | SatisfyingKW | DerivingKW
              | IfKW | ThenKW | ElseKW | DoKW
              | ImportKW | ForeignKW | NamedInstanceKW
              | EffectKW | HandlerKW | JmpKW | CtlKW | ReturnKW | ResumeKW
@@ -107,6 +107,7 @@ keyWordToken = \case
   GivenKW         -> "given"
   WithKW          -> "with"
   SatisfyingKW    -> "satisfying"
+  DerivingKW      -> "deriving"
   DoKW            -> "do"
   ImportKW        -> "import"
   ForeignKW       -> "foreign"

src/lib/PPrint.hs

@@ -638,6 +638,8 @@ instance Pretty (UTopDecl n l) where
   pretty (UInstance className bs params methods (RightB UnitB) _) =
     "instance" <+> p bs <+> p className <+> spaced params <+>
        prettyLines methods
+  pretty (UDerivingInstance className bs params) =
+    "deriving instance" <+> p bs <+> p className <+> spaced params
   pretty (UInstance className bs params methods (LeftB v) _) =
     "named-instance" <+> p v <+> ":" <+> p bs <+> p className <+> p params
         <> prettyLines methods

src/lib/SourceRename.hs

@@ -259,6 +259,10 @@ instance SourceRenamableB UTopDecl where
         sourceRenameE $ Abs conditions (PairE (ListE params) $ ListE methodDefs)
       sourceRenameB instanceName \instanceName' ->
         cont $ UInstance className' (roleExpls, conditions') params' methodDefs' instanceName' expl
+    UDerivingInstance className (roleExpls, conditions) params -> do
+      className' <- sourceRenameE className
+      Abs conditions' (ListE params') <- sourceRenameE $ Abs conditions (ListE params)
+      cont $ UDerivingInstance className' (roleExpls, conditions') params'
     UEffectDecl opTypes effName opNames -> do
       opTypes' <- mapM (\(UEffectOpType p ty) -> (UEffectOpType p) <$> sourceRenameE ty) opTypes
       sourceRenameUBinder UEffectVar effName \effName' ->
@@ -489,6 +493,7 @@ instance HasSourceNames UTopDecl where
     UInterface _ _ ~(UBindSource _ className) methodNames -> do
       S.singleton className <> sourceNames methodNames
     UInstance _ _ _ _ instanceName _ -> sourceNames instanceName
+    UDerivingInstance _ _ _ -> S.empty
     UEffectDecl _ ~(UBindSource _ effName) opNames -> do
       S.singleton effName <> sourceNames opNames
     UHandlerDecl _ _ _ _ _ _ handlerName -> sourceNames handlerName

src/lib/TraverseSourceInfo.hs

@@ -73,6 +73,7 @@ instance HasSourceInfo Occ.UsageInfo
 instance HasSourceInfo LetAnn
 instance HasSourceInfo UResumePolicy
 instance HasSourceInfo CInstanceDef
+instance HasSourceInfo CDerivingDef
 instance HasSourceInfo CTopDecl'
 
 instance HasSourceInfo AppExplicitness

src/lib/Types/Source.hs

@@ -105,6 +105,7 @@ data CTopDecl'
   -- header, givens (may be empty), methods, optional name.  The header should contain
   -- the prerequisites, class name, and class arguments.
   | CInstanceDecl CInstanceDef
+  | CDerivingDecl CDerivingDef
   deriving (Show, Generic)
 
 type CSDecl = WithSrc CSDecl'
@@ -135,6 +136,12 @@ data CInstanceDef = CInstanceDef
   (Maybe (SourceName, Maybe [Group])) -- Optional name of instance, with explicit parameters
   deriving (Show, Generic)
 
+data CDerivingDef = CDerivingDef
+  SourceName         -- interface name
+  [Group]            -- args at which we're instantiating the interface
+  (Maybe GivenClause)
+  deriving (Show, Generic)
+
 type Group = WithSrc Group'
 data Group'
   = CEmpty
@@ -341,6 +348,13 @@ data UTopDecl (n::S) (l::S) where
     -> MaybeB UAtomBinder n l    -- optional instance name
     -> AppExplicitness           -- explicitness (only relevant for named instances)
     -> UTopDecl n l
+  UDerivingInstance
+    :: SourceNameOr (Name ClassNameC) n    -- class name
+    -> UOptAnnExplBinders n l'  -- givens
+    ->   [UExpr l']                        -- class parameters
+    -- Note that no new symbols are brough into scope by a deriving instance
+    -- declaration. Hence the double occurrence of `n` in `UDecl n n`.
+    -> UTopDecl n n
   UEffectDecl
     :: [UEffectOpType n]                  -- operation types
     -> UBinder EffectNameC n l'           -- effect name