X-Git-Url: http://git.megacz.com/?a=blobdiff_plain;f=compiler%2Ftypecheck%2FTcMType.lhs;h=55b16d95bea7b44b1155fe4d8d28d83ec8cfb88b;hb=72e37dedee9e8a109ebda4b13e49b7133b530591;hp=12f3a73e01ae6f9e82d3b10ae75e21c6f2f6ce46;hpb=e07e74e5a074490d25443aeff4db4f1f299040c4;p=ghc-hetmet.git diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs index 12f3a73..55b16d9 100644 --- a/compiler/typecheck/TcMType.lhs +++ b/compiler/typecheck/TcMType.lhs @@ -422,7 +422,7 @@ zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys -> returnM (tyVarsOfTypes tys) zonkTcTyVar :: TcTyVar -> TcM TcType -zonkTcTyVar tyvar = ASSERT( isTcTyVar tyvar ) +zonkTcTyVar tyvar = ASSERT2( isTcTyVar tyvar, ppr tyvar) zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar \end{code} @@ -1137,7 +1137,7 @@ check_inst_head dflags clas tys (first_ty : _) = tys head_shape_msg = parens (text "The instance type must be of form (T a1 ... an)" $$ - text "where T is not a synonym, and a1 ... an are distinct type variables") + text "where T is not a synonym, and a1 ... an are distinct type *variables*") -- For now, I only allow tau-types (not polytypes) in -- the head of an instance decl. @@ -1183,7 +1183,11 @@ checkValidInstance tyvars theta clas inst_tys undecidableMsg]) \end{code} -Termination test: each assertion in the context satisfies +Termination test: the so-called "Paterson conditions" (see Section 5 of +"Understanding functionsl dependencies via Constraint Handling Rules, +JFP Jan 2007). + +We check that each assertion in the context satisfies: (1) no variable has more occurrences in the assertion than in the head, and (2) the assertion has fewer constructors and variables (taken together and counting repetitions) than the head.