* Now abstract over the 'a', but float out the Num (C d a) constraint
because it does not 'really' mention a. (see exactTyVarsOfType)
The arg to foo becomes
- /\a -> \t -> t+t
+ \/\a -> \t -> t+t
* So we get a dict binding for Num (C d a), which is zonked to give
a = ()
quantification, so the floated dict will still have type (C d a).
Which renders this whole note moot; happily!]
-* Then the /\a abstraction has a zonked 'a' in it.
+* Then the \/\a abstraction has a zonked 'a' in it.
All very silly. I think its harmless to ignore the problem. We'll end up with
-a /\a in the final result but all the occurrences of a will be zonked to ()
+a \/\a in the final result but all the occurrences of a will be zonked to ()
Note [Zonking to Skolem]
~~~~~~~~~~~~~~~~~~~~~~~~
check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
check_inst_head dflags clas tys
- -- If GlasgowExts then check at least one isn't a type variable
- = do checkTc (dopt Opt_TypeSynonymInstances dflags ||
- all tcInstHeadTyNotSynonym tys)
- (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
- checkTc (dopt Opt_FlexibleInstances dflags ||
- all tcInstHeadTyAppAllTyVars tys)
- (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
- checkTc (dopt Opt_MultiParamTypeClasses dflags ||
- isSingleton tys)
- (instTypeErr (pprClassPred clas tys) head_one_type_msg)
- mapM_ check_mono_type tys
+ = do { -- If GlasgowExts then check at least one isn't a type variable
+ ; checkTc (dopt Opt_TypeSynonymInstances dflags ||
+ all tcInstHeadTyNotSynonym tys)
+ (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+ ; checkTc (dopt Opt_FlexibleInstances dflags ||
+ all tcInstHeadTyAppAllTyVars tys)
+ (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+ ; checkTc (dopt Opt_MultiParamTypeClasses dflags ||
+ isSingleton tys)
+ (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+ -- May not contain type family applications
+ ; mapM_ checkTyFamFreeness tys
+
+ ; mapM_ check_mono_type tys
-- For now, I only allow tau-types (not polytypes) in
-- the head of an instance decl.
-- E.g. instance C (forall a. a->a) is rejected
-- One could imagine generalising that, but I'm not sure
-- what all the consequences might be
+ }
where
head_type_synonym_msg = parens (
; mapM_ checkTyFamFreeness typats
-- the right-hand side is a tau type
- ; checkTc (isTauTy rhs) $
- polyTyErr rhs
+ ; checkValidMonoType rhs
-- we have a decidable instance unless otherwise permitted
; undecidable_ok <- doptM Opt_UndecidableInstances
checkTyFamFreeness :: Type -> TcM ()
checkTyFamFreeness ty
= checkTc (isTyFamFree ty) $
- tyFamInstInIndexErr ty
+ tyFamInstIllegalErr ty
-- Check that a type does not contain any type family applications.
--
-- Error messages
-tyFamInstInIndexErr :: Type -> SDoc
-tyFamInstInIndexErr ty
- = hang (ptext (sLit "Illegal type family application in type instance") <>
+tyFamInstIllegalErr :: Type -> SDoc
+tyFamInstIllegalErr ty
+ = hang (ptext (sLit "Illegal type synonym family application in instance") <>
colon) 4 $
ppr ty
-polyTyErr :: Type -> SDoc
-polyTyErr ty
- = hang (ptext (sLit "Illegal polymorphic type in type instance") <> colon) 4 $
- ppr ty
-
famInstUndecErr :: Type -> SDoc -> SDoc
famInstUndecErr ty msg
= sep [msg,