From 9fa3f20ab3555ebd3d6ef0de30da8a284683fdde Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Matheus=20Magalh=C3=A3es=20de=20Alcantara?= Date: Wed, 30 Oct 2019 21:54:57 -0300 Subject: [PATCH] Support type functions referring to previous type functions --- src/Core/Builtin.hs | 2 ++ src/Types/Infer/Class.hs | 35 +++++++++++++++++++++++-------- src/Types/Kinds.hs | 10 ++++++++- tests/types/tyfun/tyfun-tyfun.ml | 20 ++++++++++++++++++ tests/types/tyfun/tyfun-tyfun.out | 9 ++++++++ 5 files changed, 66 insertions(+), 10 deletions(-) create mode 100644 tests/types/tyfun/tyfun-tyfun.ml create mode 100644 tests/types/tyfun/tyfun-tyfun.out diff --git a/src/Core/Builtin.hs b/src/Core/Builtin.hs index e107d5886..942f0f02c 100644 --- a/src/Core/Builtin.hs +++ b/src/Core/Builtin.hs @@ -146,6 +146,8 @@ builtinTyList = [ fromVar vBool , fromVar tcTypeError , fromVar tcTypeable , fromVar tcTypeRep + + , fromVar vCONS, fromVar vNIL -- XXX: tyfun-tyfun fails without this ] builtinVarList :: forall a b. (IsVar a, IsVar b) => [(a, Type b)] diff --git a/src/Types/Infer/Class.hs b/src/Types/Infer/Class.hs index 9a6026fb6..fa70bc9c8 100644 --- a/src/Types/Infer/Class.hs +++ b/src/Types/Infer/Class.hs @@ -20,7 +20,7 @@ import Data.Spanned import Data.Reason import Data.Graph import Data.Maybe -import Data.List (sortOn, partition, unzip4) +import Data.List (sortOn, partition) import Data.Char import Control.Monad.State @@ -110,8 +110,14 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do unwind (TyTuple a b) = a:unwind b unwind t = pure t + forTys (m:ms) k = do + (a, tele, d, i) <- k m + local (names %~ focus tele) $ do + (as, teles, ds, is) <- forTys ms k + pure (a:as, tele <> teles, d:ds, i:is) + forTys [] _ = pure ([], mempty, [], []) - (assocts, assocty_tele, assoct_defs, assoct_info) <- fmap unzip4 . for assoctys $ \meth@(AssocType method vs ty ann) -> do + (assocts, assocty_tele, assoct_defs, assoct_info) <- forTys assoctys $ \meth@(AssocType method vs ty ann) -> do let replaceK by (TyPi b t) = TyPi b $ replaceK by t replaceK by _ = by checkWildcard meth ty @@ -126,6 +132,7 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do kindFromArgs (TyAnnArg _ k:xs) cont = TyPi (Anon k) $ kindFromArgs xs cont kindFromArgs (_:_) _ = undefined kindFromArgs [] cont = cont + let info = TyFamInfo { _tsName = method , _tsEquations = [] , _tsConstraint = Just classConstraint @@ -138,12 +145,12 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do , info ) - ctx <- local (names %~ focus (mconcat assocty_tele <> one name k)) . for ctx $ \x -> do + ctx <- local (names %~ focus (assocty_tele <> one name k)) . for ctx $ \x -> do () <- validContext "class" classAnn x checkAgainstKind (BecauseOf clss) x tyConstraint - (fold -> scope, rows') <- local (names %~ focus (one name k <> mconcat assocty_tele)) . fmap unzip . for (getContext ctx) $ + (fold -> scope, rows') <- local (names %~ focus (one name k <> assocty_tele)) . fmap unzip . for (getContext ctx) $ \obligation -> do impty <- closeOver' vars (BecauseOf clss) $ @@ -157,7 +164,7 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do confesses (UnsatClassCon (BecauseOf clss) (head cs) (GivenContextNotEnough (fromMaybe (TyCon tyUnitName) ctx))) - local (names %~ focus (one name k <> mk_scope params <> mconcat assocty_tele)) $ do + local (names %~ focus (one name k <> mk_scope params <> assocty_tele)) $ do -- Infer the types for every method (decls, rows) <- fmap unzip . for signatures $ \meth@(MethodSig method ty _) -> do checkWildcard meth ty @@ -264,7 +271,7 @@ inferClass clss@(Class name _ ctx _ fundeps methods classAnn) = do contextMap = Map.fromList (map (\(_, _, l, t) -> (l, t)) rows') pure ( assoct_defs ++ tyDecl:map (LetStmt Public . pure) decs - , tele <> mconcat assocty_tele + , tele <> assocty_tele , info , scope , assoct_info @@ -378,7 +385,14 @@ inferInstance inst@(Instance clss ctx instHead bindings we'reDeriving ann) = con let TyApps _ classArgs = classHead - (tysyms, axioms) <- fmap unzip . for (filter (not . method) bindings) $ \bind@(TypeImpl var args exp ann) -> do + let forAx (m:ms) k = do + (syms, axs) <- k m + local (tySyms %~ extendTySyms [syms]) $ do + (syms', axs') <- forAx ms k + pure (syms:syms', axs:axs') + forAx [] _ = pure ([], []) + + (tysyms, axioms) <- forAx (filter (not . method) bindings) $ \bind@(TypeImpl var args exp ann) -> do let as (TyPi (Anon b) r) = b:as r as (TyPi _ r) = as r as _ = [] @@ -395,7 +409,9 @@ inferInstance inst@(Instance clss ctx instHead bindings we'reDeriving ann) = con local (names %~ focus (teleFromList argts)) . local (classes %~ mappend localAssums) $ do (exp, cs) <- condemn . listen $ - checkAgainstKind (BecauseOf bind) (apply (fmap unlift skolSub) exp) declared + checkAgainstKind (BecauseOf bind) + (apply (fmap unlift (instSub <> skolSub)) exp) + (apply instSub declared) let fake_clause = TyFunClause (apply skolSub (TyApps (TyCon var) (instArgs ++ map (TyVar . argName) args))) exp (ann, declared) @@ -407,7 +423,8 @@ inferInstance inst@(Instance clss ctx instHead bindings we'reDeriving ann) = con exp <- pure (deSkolFreeTy exp) unless (Seq.null cs) $ - confesses (addBlame (BecauseOf bind) (UnsatClassCon (BecauseOf bind) (cs `Seq.index` 0) (InstanceMethod ctx))) + confesses (addBlame (BecauseOf bind) + (UnsatClassCon (BecauseOf bind) (cs `Seq.index` 0) (InstanceMethod ctx))) ax <- genName con <- genName diff --git a/src/Types/Kinds.hs b/src/Types/Kinds.hs index ef1841d44..89ff6a55a 100644 --- a/src/Types/Kinds.hs +++ b/src/Types/Kinds.hs @@ -190,8 +190,16 @@ resolveClassKind stmt@(Class classcon _ ctx args _ methods _) = do let scope = one classcon kind <> tele replaceK (TyPi b t) k = TyPi b (replaceK t k) replaceK _ k = k + + forTys (m:ms) k = do + t <- k m + local (names %~ focus t) $ do + t' <- forTys ms k + pure (t <> t') + forTys [] _ = pure mempty + local (names %~ focus scope) $ do - tys <- fmap mconcat . for methods $ \case + tys <- forTys methods $ \case AssocType v _ ty _ -> do ty <- checkKind ty TyType pure (one v (replaceK kind ty)) diff --git a/tests/types/tyfun/tyfun-tyfun.ml b/tests/types/tyfun/tyfun-tyfun.ml new file mode 100644 index 000000000..346db9b43 --- /dev/null +++ b/tests/types/tyfun/tyfun-tyfun.ml @@ -0,0 +1,20 @@ +type 'a :: 'as <- Cons ('a, 'as) + +class ty_fun 'f begin + type arg + type ret + type apply ('x : arg 'f) : ret 'f +end + +type function map 'f 'xs begin + map 'f Nil = Nil + map 'f (Cons ('a, 'as)) = apply 'f 'a :: map 'f 'as +end + +type nat = Z | S of nat + +instance ty_fun S begin + type arg = nat + type ret = nat + type apply 'n = S 'n +end diff --git a/tests/types/tyfun/tyfun-tyfun.out b/tests/types/tyfun/tyfun-tyfun.out new file mode 100644 index 000000000..19e51f07b --- /dev/null +++ b/tests/types/tyfun/tyfun-tyfun.out @@ -0,0 +1,9 @@ +:: : Infer{'a : type}. 'a -> list 'a -> list 'a +ty_fun : Infer{'at : type}. 'at -> constraint +arg : Infer{'at : type}. 'at -> type +ret : Infer{'at : type}. 'at -> type +apply : arg 'f -> Infer{'at : type}. 'at -> ret 'f +map : arg 'f -> list 'at -> list (ret 'f) +nat : type +Z : nat +S : nat -> nat