Fix Trac #3540: malformed types

[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs

diff --git a/compiler/typecheck/TcMType.lhs b/compiler/typecheck/TcMType.lhs
index 525ba0d..6d6d102 100644 (file)
--- a/compiler/typecheck/TcMType.lhs
+++ b/compiler/typecheck/TcMType.lhs
@@ -415,7 +415,7 @@ occurCheckErr ty containingTy
 newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
 newCoVars spec
   = do { us <- newUniqueSupply 
-       ; return [ mkCoVar (mkSysTvName uniq (fsLit "co"))
+       ; return [ mkCoVar (mkSysTvName uniq (fsLit "co_kv"))
                           (mkCoKind ty1 ty2)
                 | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
 
@@ -1059,11 +1059,13 @@ checkValidType ctxt ty = do
 
                 ForSigCtxt _   -> gen_rank 1
                 SpecInstCtxt   -> gen_rank 1
+                ThBrackCtxt    -> gen_rank 1
 
        actual_kind = typeKind ty
 
        kind_ok = case ctxt of
                        TySynCtxt _  -> True -- Any kind will do
+                       ThBrackCtxt  -> True -- Any kind will do
                        ResSigCtxt   -> isSubOpenTypeKind actual_kind
                        ExprSigCtxt  -> isSubOpenTypeKind actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
@@ -1073,14 +1075,17 @@ checkValidType ctxt ty = do
        ubx_tup = case ctxt of
                      TySynCtxt _ | unboxed -> UT_Ok
                      ExprSigCtxt | unboxed -> UT_Ok
+                     ThBrackCtxt | unboxed -> UT_Ok
                      _                     -> UT_NotOk
 
-       -- Check that the thing has kind Type, and is lifted if necessary
-    checkTc kind_ok (kindErr actual_kind)
-
        -- Check the internal validity of the type itself
     check_type rank ubx_tup ty
 
+       -- Check that the thing has kind Type, and is lifted if necessary
+       -- Do this second, becuase we can't usefully take the kind of an 
+       -- ill-formed type such as (a~Int)
+    checkTc kind_ok (kindErr actual_kind)
+
     traceTc (text "checkValidType done" <+> ppr ty)
 
 checkValidMonoType :: Type -> TcM ()
@@ -1135,15 +1140,12 @@ check_type rank ubx_tup ty
   where
     (tvs, theta, tau) = tcSplitSigmaTy ty
    
--- Naked PredTys don't usually show up, but they can as a result of
---     {-# SPECIALISE instance Ord Char #-}
--- The Right Thing would be to fix the way that SPECIALISE instance pragmas
--- are handled, but the quick thing is just to permit PredTys here.
-check_type _ _ (PredTy sty)
-  = do { dflags <- getDOpts
-       ; check_pred_ty dflags TypeCtxt sty }
+-- Naked PredTys should, I think, have been rejected before now
+check_type _ _ ty@(PredTy {})
+  = failWithTc (text "Predicate used as a type:" <+> ppr ty)
 
 check_type _ _ (TyVarTy _) = return ()
+
 check_type rank _ (FunTy arg_ty res_ty)
   = do { check_type (decRank rank) UT_NotOk arg_ty
        ; check_type rank           UT_Ok    res_ty }
@@ -1223,13 +1225,14 @@ check_arg_type :: Rank -> Type -> TcM ()
 
 check_arg_type rank ty 
   = do { impred <- doptM Opt_ImpredicativeTypes
-       ; let rank' = if impred then ArbitraryRank  -- Arg of tycon can have arby rank, regardless
-                     else case rank of             -- Predictive => must be monotype
-                       MustBeMonoType -> MustBeMonoType 
-                       _              -> TyConArgMonoType
+       ; let rank' = case rank of          -- Predictive => must be monotype
+                       MustBeMonoType     -> MustBeMonoType  -- Monotype, regardless
+                       _other | impred    -> ArbitraryRank
+                              | otherwise -> TyConArgMonoType
                        -- Make sure that MustBeMonoType is propagated, 
                        -- so that we don't suggest -XImpredicativeTypes in
                        --    (Ord (forall a.a)) => a -> a
+                       -- and so that if it Must be a monotype, we check that it is!
 
        ; check_type rank' UT_NotOk ty
        ; checkTc (not (isUnLiftedType ty)) (unliftedArgErr ty) }
@@ -1888,8 +1891,16 @@ sizeType (ForAllTy _ ty)   = sizeType ty
 sizeTypes :: [Type] -> Int
 sizeTypes xs               = sum (map sizeType xs)
 
+-- Size of a predicate
+--
+-- Equalities are a special case.  The equality itself doesn't contribute to the
+-- size and as we do not count class predicates, we have to start with one less.
+-- This is easy to see considering that, given
+--   class C a b | a -> b
+--   type family F a
+-- constraints (C a b) and (F a ~ b) are equivalent in size.
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
 sizePred (IParam _ ty)     = sizeType ty
-sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
+sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2 - 1
 \end{code}