diff --git a/makefile b/makefile index f9c9d8ae6..8d3e33734 100644 --- a/makefile +++ b/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 diff --git a/src/lib/AbstractSyntax.hs b/src/lib/AbstractSyntax.hs index e2143fd9a..d58868034 100644 --- a/src/lib/AbstractSyntax.hs +++ b/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 diff --git a/src/lib/ConcreteSyntax.hs b/src/lib/ConcreteSyntax.hs index 06cbc702b..78a96ef1f 100644 --- a/src/lib/ConcreteSyntax.hs +++ b/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 diff --git a/src/lib/Inference.hs b/src/lib/Inference.hs index cd28d7c5e..480981d74 100644 --- a/src/lib/Inference.hs +++ b/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 ) diff --git a/src/lib/Lexing.hs b/src/lib/Lexing.hs index 0f0fc3ddb..8e6e9be90 100644 --- a/src/lib/Lexing.hs +++ b/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" diff --git a/src/lib/PPrint.hs b/src/lib/PPrint.hs index 23bc7ea60..3543142db 100644 --- a/src/lib/PPrint.hs +++ b/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 diff --git a/src/lib/SourceRename.hs b/src/lib/SourceRename.hs index 3ee3b13b1..c49db6420 100644 --- a/src/lib/SourceRename.hs +++ b/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 diff --git a/src/lib/TraverseSourceInfo.hs b/src/lib/TraverseSourceInfo.hs index 1265fbf51..329290153 100644 --- a/src/lib/TraverseSourceInfo.hs +++ b/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 diff --git a/src/lib/Types/Source.hs b/src/lib/Types/Source.hs index 21a6974ee..4e54f5f2b 100644 --- a/src/lib/Types/Source.hs +++ b/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 diff --git a/tests/deriving-instance-tests.dx b/tests/deriving-instance-tests.dx new file mode 100644 index 000000000..1c8eb8fb4 --- /dev/null +++ b/tests/deriving-instance-tests.dx @@ -0,0 +1,163 @@ + +data MyInt = MyIntCon(Int) +x: MyInt = MyIntCon 42 + + +deriving instance Show(MyInt) + +-- CHECK: "42" +show x + + +deriving instance Add(MyInt) + +-- CHECK: (MyIntCon 84) +x + x + +-- CHECK: (MyIntCon 42) +zero + x + +-- CHECK: (MyIntCon 42) +x + zero + +z : MyInt = zero + +-- CHECK: (MyIntCon 0) +z + +-- CHECK: (MyIntCon 42) +z + x + +-- CHECK: (MyIntCon 42) +x + z + + +deriving instance Eq(MyInt) + +-- CHECK: True +x == x + +-- CHECK: False +z == x + +-- CHECK: False +x == z + +-- CHECK: False +x /= x + +-- CHECK: True +z /= x + +-- CHECK: True +x /= z + + +-- Test that automatic derivation works when deriving from an instance that was +-- itself automatically derived. +data MyInt' = MyIntCon'(MyInt) +x': MyInt' = MyIntCon' x + + +deriving instance Show(MyInt') + +-- CHECK: "42" +show x' + + +deriving instance Add(MyInt') + +-- CHECK: (MyIntCon' (MyIntCon 84)) +x' + x' + +-- CHECK: (MyIntCon' (MyIntCon 42)) +zero + x' + +-- CHECK: (MyIntCon' (MyIntCon 42)) +x' + zero + +z' : MyInt' = zero + +-- CHECK: (MyIntCon' (MyIntCon 0)) +z' + +-- CHECK: (MyIntCon' (MyIntCon 42)) +z' + x' + +-- CHECK: (MyIntCon' (MyIntCon 42)) +x' + z' + + +data MyList(a) = MyListCon(List(a)) +l : MyList(Word8) = MyListCon (AsList 2 ['a', 'b']) + + +deriving instance Monoid(MyList(a)) given (a|Data) + +-- CHECK: (MyListCon "abab") +l <> l + +-- CHECK: (MyListCon "ab") +mempty <> l + +-- CHECK: (MyListCon "ab") +l <> mempty + +e : MyList(Word8) = mempty + +-- CHECK: (MyListCon "") +e + +-- CHECK: (MyListCon "ab") +e <> l + +-- CHECK: (MyListCon "ab") +l <> e + + +data MyEither(a: Type, b: Type) = + MyLeft(a) + MyRight(b) + +-- Cannot automatically derive an instance for a data type with more than one +-- constructor. +-- CHECK: Type error:User-defined ADT (MyEither a b) does not have exactly +-- CHECK-SAME: one (data) constructor that takes exactly one (data) argument +deriving instance Show(MyEither(a, b)) given (a|Show, b|Show) + +instance Show(MyEither(a, b)) given (a|Show, b|Show) + def show(y) = case y of + MyLeft(y') -> show y' + MyRight(z') -> show z' + +data MyMy(a:Type, b:Type) = MyMyCons(MyEither(a, b)) +u : MyMy Nat Float32 = MyMyCons(MyRight 23.14) + +deriving instance Show(MyMy(c, d)) given (c|Show, d|Show) + +-- CHECK: "23.1399994" +show u + + +data MyMy'(a:Type, b:Type) = MyMyCons'(MyEither(a, b)) +v : MyMy' Nat Nat = MyMyCons'(MyLeft 42) + +deriving instance Show(MyMy'(c, c)) given (c|Show) + +-- CHECK: "42" +show v + +w : MyMy' Nat Float32 = MyMyCons'(MyLeft 42) + +-- The instance of `Show` for `MyMy'(c, c)` that has been automatically derived +-- above does not yield an instance of `Show` for `MyMy'(Nat, Float32)`. +-- CHECK: Type error:Couldn't synthesize a class dictionary for: +-- CHECK-SAME: (Show (MyMy' Nat Float32)) +show w + +-- But a specific instance of `Show` for `MyMy'(Nat, Float32)` can nonetheless +-- be derived automatically. +deriving instance Show(MyMy'(Nat, Float32)) + +-- CHECK: "42" +show w