@@ -31,6 +31,7 @@ findDataConstructor dName = foldr tConsFolder Nothing
3131 [dCons] -> Just dCons
3232 _ -> error "More than one data constructor with the same name found"
3333
34+{-
3435-- | Scan the atom types and return the resultant ConstructedAtomType or error.
3536-- Used in typeFromAtomExpr to validate argument types.
3637atomTypeForDataConstructorName :: DataConstructorName -> [AtomType] -> TypeConstructorMapping -> Either RelationalError AtomType
@@ -38,8 +39,12 @@ atomTypeForDataConstructorName :: DataConstructorName -> [AtomType] -> TypeConst
3839atomTypeForDataConstructorName dConsName atomTypesIn tConsList =
3940 case findDataConstructor dConsName tConsList of
4041 Nothing -> Left (NoSuchDataConstructorError dConsName)
41− Just (tCons, dCons) ->
42− ConstructedAtomType (TCD.name tCons) <$> resolveDataConstructorTypeVars dCons atomTypesIn tConsList
42+ Just (tCons, dCons) -> do
43+ dConsVars <- resolveDataConstructorTypeVars dCons atomTypesIn tConsList
44+ let tConsVars = M.fromList (map TypeVariableType (TCD.typeVars tCons))
45+ allVars = M.union dConsVars tConsVars
46+ ConstructedAtomType (TCD.name tCons) <$> allVars
47+-}
4348
4449atomTypeForDataConstructorDefArg :: DataConstructorDefArg -> AtomType -> TypeConstructorMapping -> Either RelationalError AtomType
4550atomTypeForDataConstructorDefArg (DataConstructorDefTypeConstructorArg tCons) aType tConss = do
@@ -49,15 +54,20 @@ atomTypeForDataConstructorDefArg (DataConstructorDefTypeConstructorArg tCons) aT
4954atomTypeForDataConstructorDefArg (DataConstructorDefTypeVarNameArg _) aType _ = Right aType --any type is OK
5055
5156-- | Used to determine if the atom arguments can be used with the data constructor.
52−-- | This is the entry point for type-checking from RelationalExpression.hs.
57+-- | This is the entry point for type-checking from RelationalExpression.hs
5358atomTypeForDataConstructor :: TypeConstructorMapping -> DataConstructorName -> [AtomType] -> Either RelationalError AtomType
5459atomTypeForDataConstructor tConss dConsName atomArgTypes =
5560 --lookup the data constructor
5661 case findDataConstructor dConsName tConss of
5762 Nothing -> Left (NoSuchDataConstructorError dConsName)
58− Just (tCons, dCons) ->
63+ Just (tCons, dCons) -> do
5964 --validate that the type constructor arguments are fulfilled in the data constructor
60− ConstructedAtomType (TCD.name tCons) <$> resolveDataConstructorTypeVars dCons atomArgTypes tConss
65+ dConsVars <- resolveDataConstructorTypeVars dCons atomArgTypes tConss
66+ let tConsVars = M.fromList (map (\v -> (v, TypeVariableType v)) (TCD.typeVars tCons))
67+ allVars = M.union dConsVars tConsVars
68+ unresolvedType = ConstructedAtomType (TCD.name tCons) allVars
69+ --validateAtomType unresolvedType tConss -- do not validate here because the type may not be fully resolved at this point
70+ pure unresolvedType
6171
6272-- | Walks the data and type constructors to extract the type variable map.
6373resolveDataConstructorTypeVars :: DataConstructorDef -> [AtomType] -> TypeConstructorMapping -> Either RelationalError TypeVarMap
@@ -71,10 +81,11 @@ resolveDataConstructorTypeVars dCons@(DataConstructorDef _ defArgs) aTypeArgs tC
7181 --if any two maps have the same key and different values, this indicates a type arg mismatch
7282 let typeVarMapFolder valMap acc = case acc of
7383 Left err -> Left err
74− Right accMap -> if accMap `M.isSubmapOf` valMap then
75− Right (M.union accMap valMap)
76− else
77− Left (DataConstructorTypeVarsMismatch (DCD.name dCons) accMap valMap)
84+ Right accMap -> do
85+ case resolveAtomTypesInTypeVarMap valMap accMap of
86+ Left (TypeConstructorTypeVarMissing _) -> Left (DataConstructorTypeVarsMismatch (DCD.name dCons) accMap valMap)
87+ Left err -> Left err
88+ Right ok -> pure ok
7889 case foldr typeVarMapFolder (Right M.empty) maps of
7990 Left err -> Left err
8091 Right typeVarMaps -> pure typeVarMaps
@@ -199,6 +210,12 @@ resolveAtomType typeFromRelation unresolvedType = if typeFromRelation == unresol
199210 else
200211 Left (AtomTypeMismatchError typeFromRelation unresolvedType)
201212
213+{-
214+--walk an `AtomType` and apply the type variables in the map
215+resolveAtomTypeVars :: TypeVarMap -> AtomType -> AtomType
216+resolveAtomTypeVars tvMap typ@(TypeVariableType nam) = fromMaybe typ (M.lookup nam tvMap)
217+resolveAtomTypeVars tvMap (RelationAtomType relAttrs) =
218+-}
202219-- this could be optimized to reduce new tuple creation
203220resolveAtomTypesInTypeVarMap :: TypeVarMap -> TypeVarMap -> Either RelationalError TypeVarMap
204221resolveAtomTypesInTypeVarMap resolvedTypeMap unresolvedTypeMap = do
@@ -220,24 +237,30 @@ resolveAtomTypesInTypeVarMap resolvedTypeMap unresolvedTypeMap = do
220237 subType@(ConstructedAtomType _ _) -> do
221238 resSubType <- resolveAtomType resType subType
222239 pure (resKey, resSubType)
223− otherType -> pure (resKey, otherType)
240+ _ -> pure (resKey, resType)
224241 Nothing ->
225242 pure (resKey, resType) --swipe the missing type var from the expected map
226243 tVarList <- mapM (uncurry resolveTypePair) (M.toList resolvedTypeMap)
227244 pure (M.fromList tVarList)
228245
229246-- | See notes at `resolveTypesInTuple`. The typeFromRelation must not include any wildcards.
230−resolveTypeInAtom :: AtomType -> Atom -> Either RelationalError Atom
231−resolveTypeInAtom typeFromRelation atomIn@(ConstructedAtom dConsName _ args) = do
247+resolveTypeInAtom :: AtomType -> Atom -> TypeConstructorMapping -> Either RelationalError Atom
248+resolveTypeInAtom typeFromRelation@(ConstructedAtomType _ tvMap) atomIn@(ConstructedAtom dConsName _ args) tConss = do
232249 newType <- resolveAtomType typeFromRelation (atomTypeForAtom atomIn)
233− pure (ConstructedAtom dConsName newType args)
234−resolveTypeInAtom _ atom = Right atom
250+ case findDataConstructor dConsName tConss of
251+ Nothing -> -- the atom may have been constructed using a constructor function without a public data constructor, no further resolution is possible
252+ pure atomIn
253+ Just (_, dConsDef) -> do
254+ atomArgTypes <- resolvedAtomTypesForDataConstructorDefArgs tConss tvMap dConsDef
255+ newArgs <- mapM (\(atom, atomTyp) -> resolveTypeInAtom atomTyp atom tConss) (zip args atomArgTypes)
256+ pure (ConstructedAtom dConsName newType newArgs)
257+resolveTypeInAtom _ atom _ = Right atom
235258
236259-- | When creating a tuple, the data constructor may not complete the type constructor arguments, so the wildcard "TypeVar x" fills in the type constructor's argument. The tuple type must be resolved before it can be part of a relation, however.
237260-- Example: "Nothing" does not specify the the argument in "Maybe a", so allow delayed resolution in the tuple before it is added to the relation. Note that this resolution could cause a type error. Hardly a Hindley-Milner system.
238−resolveTypesInTuple :: Attributes -> RelationTuple -> Either RelationalError RelationTuple
239−resolveTypesInTuple resolvedAttrs (RelationTuple _ tupAtoms) = do
240− newAtoms <- mapM (\(atom, resolvedType) -> resolveTypeInAtom resolvedType atom) (zip (V.toList tupAtoms) $ map A.atomType (V.toList resolvedAttrs))
261+resolveTypesInTuple :: Attributes -> TypeConstructorMapping -> RelationTuple -> Either RelationalError RelationTuple
262+resolveTypesInTuple resolvedAttrs tConss (RelationTuple _ tupAtoms) = do
263+ newAtoms <- mapM (\(atom, resolvedType) -> resolveTypeInAtom resolvedType atom tConss) (zip (V.toList tupAtoms) $ map A.atomType (V.toList resolvedAttrs))
241264 Right (RelationTuple resolvedAttrs (V.fromList newAtoms))
242265
243266-- | Validate that the type is provided with complete type variables for type constructors.
@@ -252,7 +275,7 @@ validateAtomType typ@(ConstructedAtomType tConsName tVarMap) tConss =
252275 if not (S.null diff) then
253276 Left $ TypeConstructorTypeVarsMismatch expectedTyVarNames actualTyVarNames
254277 else
255− Right ()
278+ validateTypeVarMap tVarMap tConss
256279 _ -> Right ()
257280validateAtomType (RelationAtomType attrs) tConss = do
258281 mapM_ (\attr ->
@@ -261,8 +284,21 @@ validateAtomType (RelationAtomType attrs) tConss = do
261284validateAtomType (TypeVariableType x) _ = Left (TypeConstructorTypeVarMissing x)
262285validateAtomType _ _ = pure ()
263286
287+--ensure that all type vars are fully resolved
288+validateTypeVarMap :: TypeVarMap -> TypeConstructorMapping -> Either RelationalError ()
289+validateTypeVarMap tvMap tConss = mapM_ ((flip validateAtomType) tConss) $ (M.elems tvMap)
290+
264291validateTuple :: RelationTuple -> TypeConstructorMapping -> Either RelationalError ()
265−validateTuple (RelationTuple _ atoms) tConss = mapM_ (\a -> validateAtomType (atomTypeForAtom a) tConss) atoms
292+validateTuple (RelationTuple _ atoms) tConss = mapM_ (\a -> validateAtom a tConss) atoms
293+
294+--ensure that all types are fully resolved
295+validateAtom :: Atom -> TypeConstructorMapping -> Either RelationalError ()
296+validateAtom (RelationAtom (Relation _ tupSet)) tConss = mapM_ ((flip validateTuple) tConss) (asList tupSet)
297+validateAtom (ConstructedAtom _ dConsType atomArgs) tConss = do
298+ validateAtomType dConsType tConss
299+ mapM_ ((flip validateAtom) tConss) atomArgs
300+validateAtom _ _ = pure ()
301+
266302
267303-- | Determine if two types are equal or compatible (including special handling for TypeVar x).
268304atomTypeVerify :: AtomType -> AtomType -> Either RelationalError AtomType