From 0dc34cc0500bf322cddffafad68c933ad1f6b9d0 Mon Sep 17 00:00:00 2001 From: Jan Tikovsky Date: Mon, 18 Aug 2014 16:29:14 +0200 Subject: [PATCH] Removed expansion of record types in type error messages --- CHANGELOG.md | 2 + src/Checks/TypeCheck.hs | 154 +++++++++++++++++++++++++--------------- test/RecordTest3.curry | 22 ++++++ 3 files changed, 122 insertions(+), 56 deletions(-) create mode 100644 test/RecordTest3.curry diff --git a/CHANGELOG.md b/CHANGELOG.md index 5cb30805..4e169963 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -4,6 +4,8 @@ Change log for curry-frontend Under development ================= + * Removed expansion of record types in type error messages + * Replaced MessageM monad with CYT monads and moved CYT monads to curry-base * Implemented warnings for overlapping module aliases - fixes #14 diff --git a/src/Checks/TypeCheck.hs b/src/Checks/TypeCheck.hs index 38435f96..c92e3b00 100644 --- a/src/Checks/TypeCheck.hs +++ b/src/Checks/TypeCheck.hs @@ -4,6 +4,7 @@ Copyright : (c) 1999 - 2004 Wolfgang Lux Martin Engelke Björn Peemöller + Jan Tikovsky License : OtherLicense Maintainer : bjp@informatik.uni-kiel.de @@ -75,7 +76,7 @@ typeCheck m tcEnv tyEnv decls = execTCM check initState bindLabels tcDecls vds (tds, vds) = partition isTypeDecl decls - initState = TcState m tcEnv tyEnv idSubst emptySigEnv 0 [] + initState = TcState m tcEnv tyEnv tcEnv idSubst emptySigEnv 0 [] -- The type checker makes use of a state monad in order to maintain the type -- environment, the current substitution, and a counter which is used for @@ -85,6 +86,7 @@ data TcState = TcState { moduleIdent :: ModuleIdent -- read only , tyConsEnv :: TCEnv , valueEnv :: ValueEnv + , recordEnv :: TCEnv , typeSubst :: TypeSubst , sigEnv :: SigEnv , nextId :: Int -- automatic counter @@ -108,6 +110,12 @@ getValueEnv = S.gets valueEnv modifyValueEnv :: (ValueEnv -> ValueEnv) -> TCM () modifyValueEnv f = S.modify $ \ s -> s { valueEnv = f $ valueEnv s } +getRecordEnv :: TCM TCEnv +getRecordEnv = S.gets recordEnv + +setRecordEnv :: TCEnv -> TCM () +setRecordEnv recEnv = S.modify $ \ s -> s { recordEnv = recEnv } + getTypeSubst :: TCM TypeSubst getTypeSubst = S.gets typeSubst @@ -136,7 +144,7 @@ pre &&> suf = do execTCM :: TCM a -> TcState -> (TCEnv, ValueEnv, [Message]) execTCM tcm s = let s' = S.execState tcm s - in ( tyConsEnv s' + in ( recordEnv s' , typeSubst s' `subst` valueEnv s' , reverse $ errors s' ) @@ -144,7 +152,10 @@ execTCM tcm s = let s' = S.execState tcm s -- Defining Types: -- Before type checking starts, the types defined in the local module -- have to be entered into the type constructor environment. All type --- synonyms occurring in the definitions are fully expanded and all type +-- synonyms occurring in the definitions are fully expanded (except for +-- record types. For each record type a new type constructor is introduced +-- in the type constructor environment. The expanded record types are stored +-- in the record environment which is used during type checking) and all type -- constructors are qualified with the name of the module in which they -- are defined. This is possible because Curry does not allow (mutually) -- recursive type synonyms. In order to simplify the expansion of type @@ -154,7 +165,7 @@ execTCM tcm s = let s' = S.execState tcm s -- Note that 'bindTC' is passed the final type constructor environment in -- order to handle the expansion of type synonyms. This does not lead to a --- termination problem because 'sortTypeDecls' already has checked that there +-- termination problem because 'checkTypeDecls' already has checked that there -- are no recursive type synonyms. -- We have to be careful with existentially quantified type variables for @@ -200,27 +211,42 @@ ft m (ArrowType ty1 ty2) tcs = ft m ty1 $ ft m ty2 $ tcs ft m (RecordType fs rty) tcs = foldr (ft m) (maybe tcs (\ty -> ft m ty tcs) rty) (map snd fs) +-- The type constructor environment 'tcEnv' maintains all types +-- in fully expanded form (except for record types). +-- The record environment 'recEnv' maintains all types +-- in fully expanded form (even the record types). bindTypes :: [Decl] -> TCM () bindTypes ds = do - m <- getModuleIdent - tcEnv <- getTyConsEnv - let tcEnv' = foldr (bindTC m tcEnv') tcEnv ds + m <- getModuleIdent + tcEnv <- getTyConsEnv + recEnv <- getRecordEnv + let tcEnv' = foldr (bindTC False m tcEnv') tcEnv ds + recEnv' = foldr (bindTC True m recEnv') recEnv ds setTyConsEnv tcEnv' + setRecordEnv recEnv' -bindTC :: ModuleIdent -> TCEnv -> Decl -> TCEnv -> TCEnv -bindTC m tcEnv (DataDecl _ tc tvs cs) = +-- flag for expansion of record types +type ExpandRecordsFlag = Bool + +bindTC :: ExpandRecordsFlag -> ModuleIdent -> TCEnv -> Decl -> TCEnv -> TCEnv +bindTC _ m tcEnv (DataDecl _ tc tvs cs) = bindTypeInfo DataType m tc tvs (map (Just . mkData) cs) where mkData (ConstrDecl _ evs c tys) = mkData' evs c tys mkData (ConOpDecl _ evs ty1 op ty2) = mkData' evs op [ty1, ty2] mkData' evs c tys = DataConstr c (length evs) $ expandMonoTypes m tcEnv (cleanTVars tvs evs) tys -bindTC m tcEnv (NewtypeDecl _ tc tvs (NewConstrDecl _ evs c ty)) = +bindTC _ m tcEnv (NewtypeDecl _ tc tvs (NewConstrDecl _ evs c ty)) = bindTypeInfo RenamingType m tc tvs (DataConstr c (length evs) [ty']) where ty' = expandMonoType' m tcEnv (cleanTVars tvs evs) ty -bindTC m tcEnv (TypeDecl _ tc tvs ty) = - bindTypeInfo AliasType m tc tvs (expandMonoType' m tcEnv tvs ty) -bindTC _ _ _ = id +bindTC erflag m tcEnv t@(TypeDecl _ tc tvs ty) = + bindTypeInfo AliasType m tc tvs expTy + where expTy + | (not erflag) && isRecordDecl t = TypeConstructor qtc tys + | otherwise = expandMonoType' m tcEnv tvs ty + qtc = qualifyWith m tc + tys = map TypeVariable [0..(length tvs - 1)] +bindTC _ _ _ _ = id cleanTVars :: [Ident] -> [Ident] -> [Ident] cleanTVars tvs evs = [if tv `elem` evs then anonId else tv | tv <- tvs] @@ -265,12 +291,12 @@ bindConstrs' m tcEnv tyEnv = foldr (bindData . snd) tyEnv bindLabels :: TCM () bindLabels = do - tcEnv <- getTyConsEnv - modifyValueEnv $ bindLabels' tcEnv + recEnv <- getRecordEnv + modifyValueEnv $ bindLabels' recEnv bindLabels' :: TCEnv -> ValueEnv -> ValueEnv -bindLabels' tcEnv tyEnv = foldr (bindFieldLabels . snd) tyEnv - $ localBindings tcEnv +bindLabels' recEnv tyEnv = foldr (bindFieldLabels . snd) tyEnv + $ localBindings recEnv where bindFieldLabels (AliasType r _ (TypeRecord fs _)) env = foldr (bindField r) env fs @@ -1010,51 +1036,60 @@ unify p what doc ty1 ty2 = do theta <- getTypeSubst let ty1' = subst theta ty1 let ty2' = subst theta ty2 - m <- getModuleIdent - case unifyTypes m ty1' ty2' of + m <- getModuleIdent + recEnv <- getRecordEnv + case unifyTypes m recEnv ty1' ty2' of Left reason -> report $ errTypeMismatch p what doc m ty1' ty2' reason Right sigma -> modifyTypeSubst (compose sigma) -unifyTypes :: ModuleIdent -> Type -> Type -> Either Doc TypeSubst -unifyTypes _ (TypeVariable tv1) (TypeVariable tv2) +unifyTypes :: ModuleIdent -> TCEnv -> Type -> Type -> Either Doc TypeSubst +unifyTypes _ _ (TypeVariable tv1) (TypeVariable tv2) | tv1 == tv2 = Right idSubst | otherwise = Right (singleSubst tv1 (TypeVariable tv2)) -unifyTypes m (TypeVariable tv) ty +unifyTypes m _ (TypeVariable tv) ty | tv `elem` typeVars ty = Left (errRecursiveType m tv ty) | otherwise = Right (singleSubst tv ty) -unifyTypes m ty (TypeVariable tv) +unifyTypes m _ ty (TypeVariable tv) | tv `elem` typeVars ty = Left (errRecursiveType m tv ty) | otherwise = Right (singleSubst tv ty) -unifyTypes _ (TypeConstrained tys1 tv1) (TypeConstrained tys2 tv2) +unifyTypes _ _ (TypeConstrained tys1 tv1) (TypeConstrained tys2 tv2) | tv1 == tv2 = Right idSubst | tys1 == tys2 = Right (singleSubst tv1 (TypeConstrained tys2 tv2)) -unifyTypes m (TypeConstrained tys tv) ty = - foldr (choose . unifyTypes m ty) (Left (errIncompatibleTypes m ty (head tys))) +unifyTypes m recEnv (TypeConstrained tys tv) ty = + foldr (choose . unifyTypes m recEnv ty) (Left (errIncompatibleTypes m ty (head tys))) tys where choose (Left _) theta' = theta' choose (Right theta) _ = Right (bindSubst tv ty theta) -unifyTypes m ty (TypeConstrained tys tv) = - foldr (choose . unifyTypes m ty) (Left (errIncompatibleTypes m ty (head tys))) +unifyTypes m recEnv ty (TypeConstrained tys tv) = + foldr (choose . unifyTypes m recEnv ty) (Left (errIncompatibleTypes m ty (head tys))) tys where choose (Left _) theta' = theta' choose (Right theta) _ = Right (bindSubst tv ty theta) -unifyTypes m (TypeConstructor tc1 tys1) (TypeConstructor tc2 tys2) - | tc1 == tc2 = unifyTypeLists m tys1 tys2 -unifyTypes m (TypeArrow ty11 ty12) (TypeArrow ty21 ty22) = - unifyTypeLists m [ty11, ty12] [ty21, ty22] -unifyTypes _ (TypeSkolem k1) (TypeSkolem k2) +unifyTypes m recEnv (TypeConstructor tc1 tys1) (TypeConstructor tc2 tys2) + | tc1 == tc2 = unifyTypeLists m recEnv tys1 tys2 +unifyTypes m recEnv ty1@(TypeConstructor tc _) ty2@(TypeRecord _ _) = + maybe (Left (errIncompatibleTypes m ty1 ty2)) + (\rty -> unifyTypes m recEnv rty ty2) + (lookupRecordType tc recEnv) +unifyTypes m recEnv ty1@(TypeRecord _ _) ty2@(TypeConstructor tc _) = + maybe (Left (errIncompatibleTypes m ty1 ty2)) + (\rty -> unifyTypes m recEnv ty1 rty) + (lookupRecordType tc recEnv) +unifyTypes m recEnv (TypeArrow ty11 ty12) (TypeArrow ty21 ty22) = + unifyTypeLists m recEnv [ty11, ty12] [ty21, ty22] +unifyTypes _ _ (TypeSkolem k1) (TypeSkolem k2) | k1 == k2 = Right idSubst -unifyTypes m (TypeRecord fs1 Nothing) tr2@(TypeRecord fs2 Nothing) - | length fs1 == length fs2 = unifyTypedLabels m fs1 tr2 -unifyTypes m tr1@(TypeRecord _ Nothing) (TypeRecord fs2 (Just a2)) = +unifyTypes m recEnv (TypeRecord fs1 Nothing) tr2@(TypeRecord fs2 Nothing) + | length fs1 == length fs2 = unifyTypedLabels m recEnv fs1 tr2 +unifyTypes m recEnv tr1@(TypeRecord _ Nothing) (TypeRecord fs2 (Just a2)) = either Left (\res -> either Left (Right . compose res) - (unifyTypes m (TypeVariable a2) tr1)) - (unifyTypedLabels m fs2 tr1) -unifyTypes m tr1@(TypeRecord _ (Just _)) tr2@(TypeRecord _ Nothing) = - unifyTypes m tr2 tr1 -unifyTypes m (TypeRecord fs1 (Just a1)) tr2@(TypeRecord fs2 (Just a2)) = + (unifyTypes m recEnv (TypeVariable a2) tr1)) + (unifyTypedLabels m recEnv fs2 tr1) +unifyTypes m recEnv tr1@(TypeRecord _ (Just _)) tr2@(TypeRecord _ Nothing) = + unifyTypes m recEnv tr2 tr1 +unifyTypes m recEnv (TypeRecord fs1 (Just a1)) tr2@(TypeRecord fs2 (Just a2)) = let (fs1', rs1, rs2) = splitFields fs1 fs2 in either Left @@ -1062,11 +1097,11 @@ unifyTypes m (TypeRecord fs1 (Just a1)) tr2@(TypeRecord fs2 (Just a2)) = either Left (\res' -> Right (compose res res')) - (unifyTypeLists m [TypeVariable a1, + (unifyTypeLists m recEnv [TypeVariable a1, TypeRecord (fs1 ++ rs2) Nothing] [TypeVariable a2, TypeRecord (fs2 ++ rs1) Nothing])) - (unifyTypedLabels m fs1' tr2) + (unifyTypedLabels m recEnv fs1' tr2) where splitFields fsx fsy = split' [] [] fsy fsx split' fs1' rs1 rs2 [] = (fs1',rs1,rs2) @@ -1074,30 +1109,31 @@ unifyTypes m (TypeRecord fs1 (Just a1)) tr2@(TypeRecord fs2 (Just a2)) = maybe (split' fs1' ((l,ty):rs1) rs2 ltys) (const (split' ((l,ty):fs1') rs1 (remove l rs2) ltys)) (lookup l rs2) -unifyTypes m ty1 ty2 = Left (errIncompatibleTypes m ty1 ty2) +unifyTypes m _ ty1 ty2 = Left (errIncompatibleTypes m ty1 ty2) -unifyTypeLists :: ModuleIdent -> [Type] -> [Type] -> Either Doc TypeSubst -unifyTypeLists _ [] _ = Right idSubst -unifyTypeLists _ _ [] = Right idSubst -unifyTypeLists m (ty1 : tys1) (ty2 : tys2) = - either Left unifyTypesTheta (unifyTypeLists m tys1 tys2) +unifyTypeLists :: ModuleIdent -> TCEnv -> [Type] -> [Type] -> Either Doc TypeSubst +unifyTypeLists _ _ [] _ = Right idSubst +unifyTypeLists _ _ _ [] = Right idSubst +unifyTypeLists m recEnv (ty1 : tys1) (ty2 : tys2) = + either Left unifyTypesTheta (unifyTypeLists m recEnv tys1 tys2) where unifyTypesTheta theta = either Left (Right . flip compose theta) - (unifyTypes m (subst theta ty1) (subst theta ty2)) + (unifyTypes m recEnv (subst theta ty1) (subst theta ty2)) -unifyTypedLabels :: ModuleIdent -> [(Ident,Type)] -> Type -> Either Doc TypeSubst -unifyTypedLabels _ [] (TypeRecord _ _) = Right idSubst -unifyTypedLabels m ((l,ty):fs1) tr@(TypeRecord fs2 _) = +unifyTypedLabels :: ModuleIdent -> TCEnv -> [(Ident,Type)] -> Type + -> Either Doc TypeSubst +unifyTypedLabels _ _ [] (TypeRecord _ _) = Right idSubst +unifyTypedLabels m recEnv ((l,ty):fs1) tr@(TypeRecord fs2 _) = either Left (\r -> maybe (Left (errMissingLabel m l tr)) (\ty' -> either (const (Left (errIncompatibleLabelTypes m l ty ty'))) (Right . flip compose r) - (unifyTypes m ty ty')) + (unifyTypes m recEnv ty ty')) (lookup l fs2)) - (unifyTypedLabels m fs1 tr) -unifyTypedLabels _ _ _ = internalError "TypeCheck.unifyTypedLabels" + (unifyTypedLabels m recEnv fs1 tr) +unifyTypedLabels _ _ _ _ = internalError "TypeCheck.unifyTypedLabels" -- For each declaration group, the type checker has to ensure that no -- skolem type escapes its scope. @@ -1261,6 +1297,12 @@ fsEnv = Set.unions . map (Set.fromList . typeSkolems) . localTypes localTypes :: ValueEnv -> [Type] localTypes tyEnv = [ty | (_, Value _ _ (ForAll _ ty)) <- localBindings tyEnv] +-- Lookup record type for given type constructor identifier +lookupRecordType :: QualIdent -> TCEnv -> Maybe Type +lookupRecordType i recEnv = case qualLookupTC i recEnv of + [AliasType _ _ ty] -> Just ty + _ -> Nothing + -- --------------------------------------------------------------------------- -- Miscellaneous functions -- --------------------------------------------------------------------------- diff --git a/test/RecordTest3.curry b/test/RecordTest3.curry new file mode 100644 index 00000000..3db772c8 --- /dev/null +++ b/test/RecordTest3.curry @@ -0,0 +1,22 @@ +type R1 = { f1 :: Bool, f2 :: R2 } +type R2 = { f3 :: Int } + +type R3 a = { f4 :: String, f5 :: a } + +data T = T (R3 Int) + +-- f :: R1 -> R1 +-- f x = x + 1 + +-- g :: R3 Int -> R3 Int +-- g x = not x + +r2 :: R2 +r2 = { f3 := 0 } + +r1 :: R1 +r1 = { f1 := False, f2 := r2 } + +r3 = { f4 := "", f5 := 1 } + +e = { f2 := r3 | r1} \ No newline at end of file -- GitLab