Skip to content

GitLab

Commit 0dc34cc0 authored by Jan Rasmus Tikovsky 's avatar Jan Rasmus Tikovsky
Browse files

Removed expansion of record types in type error messages

parent e043a195
Hide whitespace changes
Inline Side-by-side
Showing with 122 additions and 56 deletions
CHANGELOG.md
View file @ 0dc34cc0
......@@ -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
......
src/Checks/TypeCheck.hs
View file @ 0dc34cc0
......@@ -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
-- ---------------------------------------------------------------------------
......
test/RecordTest3.curry 0 → 100644
View file @ 0dc34cc0
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
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment