-- -- Copyright (C) 2005 Gabriele Keller (keller@cse.unsw.edu.au) -- Stefan Wehr - http://www.stefanwehr.de -- -- This program is free software; you can redistribute it and/or -- modify it under the terms of the GNU General Public License as -- published by the Free Software Foundation; either version 2 of -- the License, or (at your option) any later version. -- -- This program is distributed in the hope that it will be useful, -- but WITHOUT ANY WARRANTY; without even the implied warranty of -- MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the GNU -- General Public License for more details. -- -- You should have received a copy of the GNU General Public License -- along with this program; if not, write to the Free Software -- Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA -- 02111-1307, USA. -- module Phrac.WellFormedness where import qualified Data.Set as Set import qualified Data.Generics as Gen import qualified Data.Typeable import qualified List import Maybe ( isJust ) import Phrac.AbstractSyntax import Phrac.Error import Phrac.Pretty import Phrac.Symtab import Phrac.Unification import Phrac.Substitution import Phrac.Entailment ( entail ) import Phrac.Configuration checkAfterKindInference :: Program -> ST () checkAfterKindInference p@(Program tydefs classDecs classInsts binds) = do debug "checking overlapping instances" mapM checkOverlappingInstances classDecs debug "checking type signatures of all methods" mapM checkMethodTypeSchemes classDecs debug "checking definitions of all associated type synonyms" mapM checkAssocTypeDefs classInsts debug ("checking if instances for all superclasses of a instance " ++ "declaration are present") mapM checkInstanceForSuperClasses classInsts debug "checking all user-supplied signatures" Gen.everywhereM (Gen.mkM checkTypeScheme') binds return () where checkTypeScheme' sc = do checkTypeScheme [] sc return sc -- type schemes in method signature must be well-formed -- {invalid_method_sig.mhs} checkMethodTypeSchemes :: ClassDec -> ST () checkMethodTypeSchemes cdec = let cid = class_name cdec c = CC $ ClassConstraint cid (map TyVar $ class_params cdec) in do debug ("checking method signatures in " ++ showPpr' cid) mapM (checkTypeScheme [c]) (map snd (class_vsigs cdec)) return () -- associated type definitions must be well-formed -- {invalid_assoc_type_def.mhs} checkAssocTypeDefs :: ClassInst -> ST () checkAssocTypeDefs ci = do debug ("checking associated type definitions in instance " ++ showInstHead ci) let rhss = map assocBind_def (inst_typeBinds ci) mapM (checkType (inst_constraints ci)) rhss return () -- Instances must not overlap. -- {overlapping.mhs} checkOverlappingInstances :: ClassDec -> ST () checkOverlappingInstances cd = do insts <- findInstances (class_name cd) checkOverlaps insts where checkOverlaps [] = return () checkOverlaps (i:is) = do l <- mapM (overlap i) is if or l then phasefail ("overlapping instances for class " ++ showPpr (class_name cd)) else checkOverlaps is overlap i1 i2 = let ts1 = inst_types i1 ts2 = inst_types i2 in do ures <- runUnify [] (map (\ (x,y) -> x :=: y) (zip ts1 ts2)) case ures of Left err -> return False Right (eqc, _) -> if null eqc then return True else panic ("Unification succeeded with the " ++ "following equality " ++ "constraints when checking for " ++ "overlapping instances: " ++ showCommaListed eqc) -- given: instance declaration (Phi => C t) -- check if (S t) holds for all superclasses S of C. -- {missing_superclass_instance.phc, missing_superclass_instance2.phc} checkInstanceForSuperClasses :: ClassInst -> ST () checkInstanceForSuperClasses ci = do let cid = inst_class ci cdec <- findClass cid let constrs = inst_constraints ci subst = substFromAssocs (zip (class_params cdec) (inst_types ci)) supers <- findAllSuperConstraints cid mapM (checkEntailment subst constrs) supers return () where checkEntailment :: TypeSubst -> [Constraint] -> ClassConstraint -> ST () checkEntailment subst ps (ClassConstraint cid ts) = do let cc = CC $ ClassConstraint cid (applySubst subst ts) debug ("checking if context " ++ showPpr' ps ++ " entails " ++ "superclass constraint " ++ showPpr' cc) b <- entail ps cc if not b then phasefail ("cannot entail " ++ showPpr' cc ++ " when checking instance declaration " ++ showInstHead ci) else return () check :: Program -> ST () check p@(Program tydefs classDecs classInsts binds) = do display "checking class declarations" mapM checkClassDec classDecs Gen.everywhereM (Gen.mkM checkClassConstraint) p display "checking instance declarations" mapM checkInstanceDec classInsts display "checking bindings" Gen.everywhereM (Gen.mkM checkBind) p display "checking associated type applications" Gen.everywhereM (Gen.mkM checkAssocTypeApplication) p return () -- class hierarchy must be acyclic -- {cyclic_class_hierarchy.mhs} -- => checked while building symtab --------------------------------------------------- -- well-formedness checks for class declarations -- --------------------------------------------------- checkClassDec :: ClassDec -> ST () checkClassDec d = do checkClassContext d checkTypeSigs d checkMethodSigs d return () -- The context of the class may constraint only type variables mentioned -- in the class head. -- {constraining_unbound_var1.mhs} checkClassContext :: ClassDec -> ST () checkClassContext (ClassDec id param constrs _ _ _) = mapM_ checkConstr constrs where checkConstr (ClassConstraint _ ts) = if all isTypeVar ts then return () -- syntax transformation guarantees that only -- class variables are constrained else return () {- phasefail ("illegal context for class " ++ showPpr id ++ ": only type variables can be constrained") -} -- An associated type synonym must be parameterised over all -- parameters of the class, and these type variables must come first, -- and be in the same order as in the class. -- {illegal_assoc_decl1.mhs, illegal_assoc_decl2.mhs} -- types of fixed associated type synonyms must be well-formed -- (see tests in tests/fixed-assoc-types) checkTypeSigs (ClassDec id classParams constrs tsigs _ _) = mapM_ checkTypeSig tsigs where checkTypeSig (AssocTypeSig aid ps t) = do debug ("checking associated type synonym " ++ showPpr' aid) let n = length classParams indices = take n ps params = drop n ps if indices /= classParams then phasefail ("signature of associated type synonym " ++ showPpr aid ++ " does not repeat the class " ++ "parameters") else return () case t of Nothing -> return () Just t' -> do checkType (map CC constrs) t' conf <- getConfiguration if typeSynonymTermination conf == DecreasingConstructorCount then checkDecreasingAssocTypeDefinition (AssocTypeBind aid (map TyVar indices) params t' AssocTypeNotAbstract) else return () -- The signature of a method must not constrain the class parameter. -- The class parameter must be contained in Fixv(simga) for all -- method signatures sigma. -- {constrain_class_param.mhs, ambiguous1.mhs} checkMethodSigs (ClassDec id params _ _ msigs _) = do mapM checkClassParamUnconstrained msigs mapM checkFixv msigs mapM checkEqConstraints msigs return () where checkClassParamUnconstrained (mid, TypeScheme _ (QualifiedType cs _)) = if not $ null (params `List.intersect` freeTypeVarsList cs) then phasefail ("signature of method " ++ showPpr mid ++ " of class " ++ showPpr id ++ " constrains some class parameter") else return () checkFixv (mid, sc) = if not $ Set.fromList params `Set.isSubsetOf` fixedTypeVars sc then phasefail ("signature of method " ++ showPpr mid ++ " of class " ++ showPpr id ++ " is invalid.") else return () checkEqConstraints (_, TypeScheme _ (QualifiedType cs _)) = do mapM checkConstraint cs return () ------------------------------------------------------ -- well-formedness checks for instance declarations -- ------------------------------------------------------ checkInstanceDec :: ClassInst -> ST () checkInstanceDec ci@(ClassInst clazz tys constrs tyBinds methodBinds _) = do cdec <- findClass clazz if length (class_params cdec) /= length tys then phasefail ("illegal instance declaration for class " ++ showPpr' clazz ++ ": wrong number of arguments") else return () mapM checkConstraint constrs checkIfAllAssocTypesAreDefined ci checkIfAllMethodsAreDefined ci checkConstructorBased ci checkInstanceConstraints ci mapM (checkAssocTypeHead ci) tyBinds mapM checkAssocTypeDefinition tyBinds return () -- Instance heads must be constructor based, a single variable is not allowed. -- All variables in the instance head must be distinct. -- {illegal_instance_head.mhs, instance_for_tyvar.mhs} checkConstructorBased :: ClassInst -> ST () checkConstructorBased (ClassInst clazz tys _ _ _ _) = let vars = concatMap allTypeVars tys in do if length vars /= length (List.nub vars) then phasefail ("duplicate type variable in head of instance " ++ "for class " ++ showPpr clazz) else return () if all isTypeVar tys then phasefail ("illegal instance definition: all parameters " ++ "are type variables") else return () -- All constraints in the instance context must be of the form C a1 .. aN -- (where C is a class and the aI are type variables) or T a1..aN = t -- (where T a1..aN is the saturated application of an associated type synonym -- and t is a type but not a single variable; all arguments to synonym -- applications in t must be variables). -- {illegal_instance_constraint1.mhs, illegal_instance_constraint2.mhs, -- illegal_instance_constraint3.mhs} checkInstanceConstraints (ClassInst clazz _ constrs _ _ _) = do mapM checkConstraint constrs return () where checkConstraint c@(CC (ClassConstraint _ tys)) = if all isTypeVar tys then return () else phasefail ("illegal constraint in instance declaration for " ++ "class " ++ showPpr clazz ++ ": " ++ showPpr c) checkConstraint c@(EC (EqConstraint (AssocType _ ps) t)) = let isTyVar (TyVar _) = True isTyVar _ = False allSynArgs = Gen.everything (++) ([] `Gen.mkQ` synArgs) t synArgs (AssocType _ ps) = ps cond1 = and (map isTyVar ps) cond2 = not (isTyVar t) cond3 = and (map isTyVar allSynArgs) in if cond1 && cond2 && cond3 then return () else phasefail ("illegal constraint in instance declaration " ++ "for class " ++ showPpr clazz ++ ": " ++ showPpr c) -- All non-fixed associated type synonyms of the corresponding class must -- be defined, the fixed type synonyms must not be defined. -- {missing_assoc_type.mhs} checkIfAllAssocTypesAreDefined (ClassInst classId _ _ tyBinds _ _) = do clazz <- findClass classId let sigs = filter (\sig -> not $ isJust (assocSig_fixed sig)) (class_tsigs clazz) if length sigs /= (length tyBinds) then phasefail ("illegal instance declaration for class " ++ showPpr classId ++ ": type synonyms do not match") else return () let sigNames = List.sort $ map assocSig_name sigs bindNames = List.sort $ map assocBind_name tyBinds if sigNames /= bindNames then phasefail ("illegal instance declaration for class " ++ showPpr classId ++ ": type synonyms do not match") else return () -- All methods of the corresponding class must be defined. -- {missing_method.mhs} checkIfAllMethodsAreDefined (ClassInst classId _ _ _ vbinds _) = do clazz <- findClass classId let vsigs = class_vsigs clazz if length vsigs /= length vbinds then phasefail ("illegal instance declaration for class " ++ showPpr classId ++ ": methods do not match") else return () mapM checkMethodDefinition (zip (List.sortBy cmpVsig vsigs) (List.sortBy cmpVbind vbinds)) return () where cmpVsig (id1,_) (id2,_) = id1 `compare` id2 cmpVbind b1 b2 = vbind_name b1 `compare` vbind_name b2 checkMethodDefinition ((id,_), mb) | id == vbind_name mb = return () | otherwise = phasefail ("illegal instance declaration for class " ++ showPpr classId ++ ": methods do not match") -- The head of the definition of an associated type synonym must repeat -- the instance parameters and all other parameters must be simple -- variables. The overall number of parameters must be the same as in the -- class declaration. -- {not_repeating_params.mhs, param_number_not_ok.mhs} checkAssocTypeHead :: ClassInst -> AssocTypeBind -> ST () checkAssocTypeHead ci at = do let id = assocBind_name at AssocTypeSig _ params _ <- findAssocTypeSig id if length params /= (length $ assocBind_indices at) + (length $ assocBind_params at) then phasefail ("wrong number of arguments in definition of " ++ "associated type synonym " ++ showPpr id) else return () if assocBind_indices at /= inst_types ci then phasefail ("definiton of associated type synonym must " ++ "repeat the type of the instance head") else return () checkAssocTypeDefinition :: AssocTypeBind -> ST () checkAssocTypeDefinition atb@(AssocTypeBind id p ps ty _) = do -- Definitions of ATSs must be constructor based (trivial because -- instance heads must be constructor based) ok -- Definitions of ATSs must be left linear (trivial because -- left-linearity of the index of the AT is ensured by the -- left-linearity of the instance head and the syntax transformation -- makes sure that all other type variables are distinct. -- {not_left_linear.mhs} ok -- Definitions must be non-overlapping (trivial because instances must -- be non-overlapping). ok -- Definitions must be decreasing and linear in arguments to synonym -- applications. -- {not_decreasing.mhs, not_linear_in_args.mhs} conf <- getConfiguration if typeSynonymTermination conf == DecreasingConstructorCount then checkDecreasingAssocTypeDefinition atb else return () where ok = return () checkDecreasingAssocTypeDefinition (AssocTypeBind id indices params ty _) = do let m = sum (map dataConstructorCount indices) n = if length (allAssocTypes ty) == 0 then -1 else maximum (map assocTypeDataConstructorCount (allAssocTypes ty)) if n >= m then phasefail ("Definition of associated type synonym " ++ showPpr id ++ " is not decreasing. Number of " ++ "data constructors in definition head: " ++ show m ++ ". Number of data constructors on the " ++ "right side: " ++ show n) else return () mapM (\args -> if length args /= length (List.nub args) then phasefail ("Definition of associated type synonym " ++ showPpr id ++ " contains a non-linear " ++ "type synonym application") else return ()) (map allTypeVars (allAssocTypes ty :: [AssocType])) return () where assocTypeDataConstructorCount (AssocType _ ps) = sum (map dataConstructorCount ps) allAssocTypesArgs ty = map (\ (AssocType _ ps) -> ps) (allAssocTypes ty) dataConstructorCount = Gen.everything (+) (0 `Gen.mkQ` (\t -> case t of TyConstruct _ -> 1 _ -> 0)) --------------------------------------------------------- -- well-formedness checks for associated type synonyms -- --------------------------------------------------------- -- all applications of associated type synonyms must be saturated -- {not_saturated1.mhs, not_saturated2.mh, not_saturated3.mhs} checkAssocTypeApplication :: AssocType -> ST AssocType checkAssocTypeApplication at = do sig <- findAssocTypeSig (assoc_name at) if length (assocSig_params sig) /= length (assoc_params at) then phasefail ("application `" ++ showPpr at ++ "' of associated " ++ "type synonym is not saturated") else return at -------------------------------------------------------------- -- well-formedness checks for user-supplied type annotations - -------------------------------------------------------------- -- for all signatures 'forall a1..aN . rho': -- 'a1..aN `intersect` Free(rho)' must be a subset of Fixv(rho) -- => we check this after type inference, because we have to do it for -- ALL signatures {- checkIfSignatureAmbiguous :: TypeScheme -> ST () checkIfSignatureAmbiguous ts@(TypeScheme alphas rho) = if not $ (Set.fromList alphas `Set.intersection` freeTypeVars rho) `Set.isSubsetOf` fixedTypeVars rho then phasefail ("signature `" ++ showPpr ts ++ "' is ambiguous") else return () -} -- in equality constraints, the first n arguments (where n is the number of -- class parameter of the class defining the synonym) of the type synonym -- applications in the left side must be type variables. -- {eq_constraint1.mhs, eq_constraint2.mhs, eq_constraint3.mhs, -- eq_constraint4.mhs} checkConstraint :: Constraint -> ST () checkConstraint (CC _) = return () checkConstraint (EC (EqConstraint (AssocType name params) _)) = do n <- getAssocIndexCount name if not (all isTypeVar (take n params)) then phasefail ("invalid associated type synonym `" ++ showPpr name ++ "' in equality constraint (one of the index " ++ "parameters is not a variable)") else return () ---------------------- -- checks for binds -- ---------------------- checkBind :: ValBind -> ST ValBind checkBind b@(ValBind i (Just (TypeScheme _ (QualifiedType cs _))) _ e _) = do debug ("checking binding " ++ showPpr' i) mapM checkConstraint cs return b checkBind b@(_) = return b ---------------------- -- checks for types -- ---------------------- -- the `Theta |- tau' relation in figure 2. -- checkTypeScheme uses the program's class and equality constraints -- implicitly, i.e. `checkTypeScheme cs t' checks if type scheme t is -- well-formed wrt the program constraints and the constraints cs. -- FIXME: The constraints cs are not quantified (I simple assume an empty -- quantifier list). checkTypeScheme :: [Constraint] -> TypeScheme -> ST () checkTypeScheme cs sc@(TypeScheme quants (QualifiedType cs' t)) = do -- first ensure that no quantifiers is free in the environment -- for computing the free variables of the program environment, we -- only have to consider equality constraints (class constraints -- do not have free variables) eqDefs <- getGlobalEqualities let frees = freeTypeVars eqDefs `Set.union` freeTypeVars cs inters = Set.fromList quants `Set.intersection` frees if not $ Set.null inters then phasefail ("Type scheme " ++ showPpr' sc ++ " is not well-formed" ++ ": it quantifies over some variables contained in " ++ "the environment: " ++ showCommaListed (Set.toList inters)) else return () checkType (cs ++ cs') t checkType :: [Constraint] -> Type -> ST () checkType _ (TyVar _) = return () checkType cs (TyApp t1 t2) = do checkType cs t1 checkType cs t2 checkType _ (TyConstruct _) = return () checkType cs at@(TyAssoc (AssocType id params)) = do mapM (checkType cs) params cd <- findClassOfAssocType id let indices = take (length $ class_params cd) params let c = CC $ ClassConstraint (class_name cd) indices e <- entail cs c if not e then phasefail ("illegal associated type application: " ++ showPpr' at ++ ". Cannot deduce " ++ showPpr' c ++ " from program context and " ++ showCommaListed cs) else return () -- check that a class constraint uses the right number of arguments checkClassConstraint :: ClassConstraint -> ST ClassConstraint checkClassConstraint cc@(ClassConstraint id params) = do cdec <- findClass id if length params /= length (class_params cdec) then phasefail ("illegal class constraint: " ++ showPpr' cc ++ ": wrong number of arguments") else return cc -- -- Helpers -- allAssocTypes :: (Gen.Data a) => a -> [AssocType] allAssocTypes x = Gen.everything (++) ([] `Gen.mkQ` (\ a@(AssocType _ _) -> [a])) x allTypeVars :: (Gen.Data a) => a -> [TypeVarId] allTypeVars x = Gen.everything (++) ([] `Gen.mkQ` allTypeVars) x where allTypeVars (TyVar id) = [id] allTypeVars _ = []