projects
/
ghc-hetmet.git
/ blobdiff
commit
grep
author
committer
pickaxe
?
search:
re
summary
|
shortlog
|
log
|
commit
|
commitdiff
|
tree
raw
|
inline
| side by side
Some tyvars were being introduced in the environment via the thunk bindings '_ti...
[ghc-hetmet.git]
/
compiler
/
typecheck
/
TcMType.lhs
diff --git
a/compiler/typecheck/TcMType.lhs
b/compiler/typecheck/TcMType.lhs
index
f206b5e
..
55b16d9
100644
(file)
--- a/
compiler/typecheck/TcMType.lhs
+++ b/
compiler/typecheck/TcMType.lhs
@@
-81,7
+81,7
@@
import UniqSupply
import SrcLoc
import Outputable
import SrcLoc
import Outputable
-import Control.Monad ( when )
+import Control.Monad ( when, unless )
import Data.List ( (\\) )
\end{code}
import Data.List ( (\\) )
\end{code}
@@
-422,7
+422,7
@@
zonkTcTyVarsAndFV tyvars = mappM zonkTcTyVar tyvars `thenM` \ tys ->
returnM (tyVarsOfTypes tys)
zonkTcTyVar :: TcTyVar -> TcM TcType
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}
zonk_tc_tyvar (\ tv -> returnM (TyVarTy tv)) tyvar
\end{code}
@@
-826,12
+826,15
@@
check_tau_type rank ubx_tup ty@(TyConApp tc tys)
-- type Foo a = Tree [a]
-- f :: Foo a b -> ...
; case tcView ty of
-- type Foo a = Tree [a]
-- f :: Foo a b -> ...
; case tcView ty of
- Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
- Nothing -> failWithTc arity_msg
+ Just ty' -> check_tau_type rank ubx_tup ty' -- Check expansion
+ Nothing -> unless (isOpenTyCon tc -- No expansion if open
+ && tyConArity tc <= length tys) $
+ failWithTc arity_msg
; gla_exts <- doptM Opt_GlasgowExts
; gla_exts <- doptM Opt_GlasgowExts
- ; if gla_exts then
- -- If -fglasgow-exts then don't check the type arguments
+ ; if gla_exts && not (isOpenTyCon tc) then
+ -- If -fglasgow-exts then don't check the type arguments of
+ -- *closed* synonyms.
-- This allows us to instantiate a synonym defn with a
-- for-all type, or with a partially-applied type synonym.
-- e.g. type T a b = a
-- This allows us to instantiate a synonym defn with a
-- for-all type, or with a partially-applied type synonym.
-- e.g. type T a b = a
@@
-1133,8
+1136,8
@@
check_inst_head dflags clas tys
where
(first_ty : _) = tys
where
(first_ty : _) = tys
- head_shape_msg = parens (text "The instance type must be of form (T a b c)" $$
- text "where T is not a synonym, and a,b,c are distinct type variables")
+ 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*")
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
@@
-1169,7
+1172,7
@@
checkValidInstance tyvars theta clas inst_tys
-- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
; when (gla_exts && not undecidable_ok) $
-- Check that instance inference will terminate (if we care)
-- For Haskell 98, checkValidTheta has already done that
; when (gla_exts && not undecidable_ok) $
- mapM_ failWithTc (checkInstTermination inst_tys theta)
+ mapM_ addErrTc (checkInstTermination inst_tys theta)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
-- The Coverage Condition
; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
@@
-1180,7
+1183,11
@@
checkValidInstance tyvars theta clas inst_tys
undecidableMsg])
\end{code}
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.
(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.