Fix recursive superclasses (again). Fixes Trac #4809.
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index 950d733..ef4ad34 100644 (file)
@@ -26,16 +26,15 @@ module TcMType (
   -- Creating new evidence variables
   newEvVar, newCoVar, newEvVars,
   newWantedCoVar, writeWantedCoVar, readWantedCoVar, 
-  newIP, newDict, newSelfDict, isSelfDict,
+  newIP, newDict, newSilentGiven, isSilentEvVar,
 
-  newWantedEvVar, newWantedEvVars, 
-  newKindConstraint,
+  newWantedEvVar, newWantedEvVars,
   newTcEvBinds, addTcEvBind,
 
   --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstTyVars, tcInstSigTyVars,
-  tcInstType, tcInstSigType,
+  tcInstType, tcInstSigType, instMetaTyVar,
   tcInstSkolTyVars, tcInstSkolTyVar, tcInstSkolType, 
   tcSkolSigType, tcSkolSigTyVars, 
 
@@ -43,15 +42,15 @@ module TcMType (
   -- Checking type validity
   Rank, UserTypeCtxt(..), checkValidType, checkValidMonoType,
   SourceTyCtxt(..), checkValidTheta, 
-  checkValidInstHead, checkValidInstance, 
-  checkInstTermination, checkValidTypeInst, checkTyFamFreeness, 
+  checkValidInstance,
+  checkValidTypeInst, checkTyFamFreeness,
   arityErr, 
   growPredTyVars, growThetaTyVars, validDerivPred,
 
   --------------------------------
   -- Zonking
   zonkType, mkZonkTcTyVar, zonkTcPredType, 
-  zonkTcTypeCarefully,
+  zonkTcTypeCarefully, skolemiseUnboundMetaTyVar,
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkSigTyVar,
   zonkQuantifiedTyVar, zonkQuantifiedTyVars,
   zonkTcType, zonkTcTypes, zonkTcThetaType,
@@ -135,17 +134,6 @@ newWantedEvVars theta = mapM newWantedEvVar theta
 newWantedCoVar :: TcType -> TcType -> TcM CoVar 
 newWantedCoVar ty1 ty2 = newCoVar ty1 ty2
 
--- We used to create a mutable co-var
-{-
--- A wanted coercion variable is a MetaTyVar
--- that can be filled in with its binding
-  = do { uniq <- newUnique 
-       ; ref <- newMutVar Flexi 
-       ; let name = mkSysTvName uniq (fsLit "c")
-             kind = mkPredTy (EqPred ty1 ty2) 
-       ; return (mkTcTyVar name kind (MetaTv TauTv ref)) }
--}
-
 --------------
 newEvVar :: TcPredType -> TcM EvVar
 -- Creates new *rigid* variables for predicates
@@ -175,29 +163,23 @@ newName occ
        ; return (mkInternalName uniq occ loc) }
 
 -----------------
-newKindConstraint :: Type -> Kind -> TcM (CoVar, Type)
--- Create a new wanted CoVar that constrains the type
--- to have the specified kind
-newKindConstraint ty kind
-  = do { ty_k <- newFlexiTyVarTy kind
-       ; co_var <- newWantedCoVar ty ty_k
-       ; return (co_var, ty_k) }
-
------------------
-newSelfDict :: Class -> [TcType] -> TcM DictId
--- Make a dictionary for "self". It behaves just like a normal DictId
--- except that it responds True to isSelfDict
+newSilentGiven :: PredType -> TcM EvVar
+-- Make a dictionary for a "silent" given dictionary
+-- Behaves just like any EvVar except that it responds True to isSilentDict
 -- This is used only to suppress confusing error reports
-newSelfDict cls tys 
+newSilentGiven (ClassP cls tys)
   = do { uniq <- newUnique
-       ; let name = mkSystemName uniq selfDictOcc
+       ; let name = mkSystemName uniq (mkDictOcc (getOccName cls))
        ; return (mkLocalId name (mkPredTy (ClassP cls tys))) }
+newSilentGiven (EqPred ty1 ty2)
+  = do { uniq <- newUnique
+       ; let name = mkSystemName uniq (mkTyVarOccFS (fsLit "co"))
+       ; return (mkCoVar name (mkPredTy (EqPred ty1 ty2))) }
+newSilentGiven pred@(IParam {})
+  = pprPanic "newSilentDict" (ppr pred) -- Implicit parameters rejected earlier
 
-selfDictOcc :: OccName
-selfDictOcc = mkVarOcc "self"
-
-isSelfDict :: EvVar -> Bool
-isSelfDict v = isSystemName (Var.varName v)
+isSilentEvVar :: EvVar -> Bool
+isSilentEvVar v = isSystemName (Var.varName v)
   -- Notice that all *other* evidence variables get Internal Names
 \end{code}
 
@@ -305,6 +287,7 @@ newMetaTyVar meta_info kind
        ; let name = mkSysTvName uniq fs 
              fs = case meta_info of
                        TauTv   -> fsLit "t"
+                       TcsTv   -> fsLit "u"
                        SigTv _ -> fsLit "a"
        ; return (mkTcTyVar name kind (MetaTv meta_info ref)) }
 
@@ -497,10 +480,10 @@ zonkTcTypeCarefully ty
       | otherwise
       = ASSERT( isTcTyVar tv )
        case tcTyVarDetails tv of
-         SkolemTv {}    -> return (TyVarTy tv)
+         SkolemTv {}  -> return (TyVarTy tv)
          FlatSkol ty  -> zonkType (zonk_tv env_tvs) ty
-         MetaTv _ ref   -> do { cts <- readMutVar ref
-                              ; case cts of    
+         MetaTv _ ref -> do { cts <- readMutVar ref
+                            ; case cts of    
                                   Flexi       -> return (TyVarTy tv)
                                   Indirect ty -> zonkType (zonk_tv env_tvs) ty }
 
@@ -513,11 +496,11 @@ zonkTcTyVar :: TcTyVar -> TcM TcType
 zonkTcTyVar tv
   = ASSERT2( isTcTyVar tv, ppr tv )
     case tcTyVarDetails tv of
-      SkolemTv {}    -> return (TyVarTy tv)
+      SkolemTv {}  -> return (TyVarTy tv)
       FlatSkol ty  -> zonkTcType ty
-      MetaTv _ ref   -> do { cts <- readMutVar ref
-                          ; case cts of    
-                              Flexi       -> return (TyVarTy tv)
+      MetaTv _ ref -> do { cts <- readMutVar ref
+                        ; case cts of    
+                              Flexi       -> return (TyVarTy tv)
                               Indirect ty -> zonkTcType ty }
 
 zonkTcTypeAndSubst :: TvSubst -> TcType -> TcM TcType
@@ -557,8 +540,6 @@ zonkQuantifiedTyVars :: [TcTyVar] -> TcM [TcTyVar]
 zonkQuantifiedTyVars = mapM zonkQuantifiedTyVar
 
 zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
--- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
---
 -- The quantified type variables often include meta type variables
 -- we want to freeze them into ordinary type variables, and
 -- default their kind (e.g. from OpenTypeKind to TypeKind)
@@ -569,35 +550,39 @@ zonkQuantifiedTyVar :: TcTyVar -> TcM TcTyVar
 --
 -- We leave skolem TyVars alone; they are immutable.
 zonkQuantifiedTyVar tv
-  | ASSERT2( isTcTyVar tv, ppr tv ) 
-    isSkolemTyVar tv 
-  = do { kind <- zonkTcType (tyVarKind tv)
-       ; return $ setTyVarKind tv kind
-       }
+  = ASSERT2( isTcTyVar tv, ppr tv ) 
+    case tcTyVarDetails tv of
+      FlatSkol {} -> pprPanic "zonkQuantifiedTyVar" (ppr tv)
+      SkolemTv {} -> do { kind <- zonkTcType (tyVarKind tv)
+                        ; return $ setTyVarKind tv kind }
        -- It might be a skolem type variable, 
        -- for example from a user type signature
 
-  | otherwise  -- It's a meta-type-variable
-  = do { details <- readMetaTyVar tv
-
-       -- Create the new, frozen, skolem type variable
-        -- We zonk to a skolem, not to a regular TcVar
-        -- See Note [Zonking to Skolem]
-        ; uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
+      MetaTv _ _ref -> 
+#ifdef DEBUG               
+                       -- [Sept 04] Check for non-empty.  
+                       -- See note [Silly Type Synonym]
+                      (readMutVar _ref >>= \cts -> 
+                       case cts of 
+                             Flexi -> return ()
+                             Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
+                                            return ()) >>
+#endif
+                      skolemiseUnboundMetaTyVar UnkSkol tv 
+                             
+skolemiseUnboundMetaTyVar :: SkolemInfo -> TcTyVar -> TcM TyVar
+-- We have a Meta tyvar with a ref-cell inside it
+-- Skolemise it, including giving it a new Name, so that
+--   we are totally out of Meta-tyvar-land
+-- We create a skolem TyVar, not a regular TyVar
+--   See Note [Zonking to Skolem]
+skolemiseUnboundMetaTyVar skol_info tv
+  = ASSERT2( isMetaTyVar tv, ppr tv ) 
+    do { uniq <- newUnique  -- Remove it from TcMetaTyVar unique land
        ; let final_kind = defaultKind (tyVarKind tv)
               final_name = setNameUnique (tyVarName tv) uniq
-             final_tv   = mkSkolTyVar final_name final_kind UnkSkol
-
-       -- Bind the meta tyvar to the new tyvar
-       ; case details of
-           Indirect ty -> WARN( True, ppr tv $$ ppr ty ) 
-                          return ()
-               -- [Sept 04] I don't think this should happen
-               -- See note [Silly Type Synonym]
-
-           Flexi -> writeMetaTyVar tv (mkTyVarTy final_tv)
-
-       -- Return the new tyvar
+             final_tv   = mkSkolTyVar final_name final_kind skol_info
+       ; writeMetaTyVar tv (mkTyVarTy final_tv)
        ; return final_tv }
 \end{code}
 
@@ -702,10 +687,8 @@ simplifier knows how to deal with.
 -- For tyvars bound at a for-all, zonkType zonks them to an immutable
 --     type variable and zonks the kind too
 
-zonkType :: (TcTyVar -> TcM Type)      -- What to do with unbound mutable type variables
-                                       -- see zonkTcType, and zonkTcTypeToType
-         -> TcType
-        -> TcM Type
+zonkType :: (TcTyVar -> TcM Type)  -- What to do with TcTyVars
+         -> TcType -> TcM Type
 zonkType zonk_tc_tyvar ty
   = go ty
   where
@@ -745,7 +728,7 @@ zonkType zonk_tc_tyvar ty
                                   ty2' <- go ty2
                                   return (EqPred ty1' ty2')
 
-mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an unbound mutable var
+mkZonkTcTyVar :: (TcTyVar -> TcM Type) -- What to do for an *mutable Flexi* var
              -> TcTyVar -> TcM TcType
 mkZonkTcTyVar unbound_var_fn tyvar 
   = ASSERT( isTcTyVar tyvar )
@@ -1155,10 +1138,12 @@ check_pred_ty dflags ctxt pred@(ClassP cls tys)
     how_to_allow = parens (ptext (sLit "Use -XFlexibleContexts to permit this"))
 
 
-check_pred_ty dflags _ pred@(EqPred ty1 ty2)
+check_pred_ty dflags ctxt pred@(EqPred ty1 ty2)
   = do {       -- Equational constraints are valid in all contexts if type
                -- families are permitted
        ; checkTc (xopt Opt_TypeFamilies dflags) (eqPredTyErr pred)
+       ; checkTc (case ctxt of ClassSCCtxt {} -> False; _ -> True)
+                 (eqSuperClassErr pred)
 
                -- Check the form of the argument types
        ; checkValidMonoType ty1
@@ -1315,11 +1300,16 @@ checkThetaCtxt ctxt theta
   = vcat [ptext (sLit "In the context:") <+> pprTheta theta,
          ptext (sLit "While checking") <+> pprSourceTyCtxt ctxt ]
 
+eqSuperClassErr :: PredType -> SDoc
+eqSuperClassErr pred
+  = hang (ptext (sLit "Alas, GHC 7.0 still cannot handle equality superclasses:"))
+       2 (ppr pred)
+
 badPredTyErr, eqPredTyErr, predTyVarErr :: PredType -> SDoc
-badPredTyErr sty = ptext (sLit "Illegal constraint") <+> pprPred sty
-eqPredTyErr  sty = ptext (sLit "Illegal equational constraint") <+> pprPred sty
-                  $$
-                  parens (ptext (sLit "Use -XTypeFamilies to permit this"))
+badPredTyErr pred = ptext (sLit "Illegal constraint") <+> pprPred pred
+eqPredTyErr  pred = ptext (sLit "Illegal equational constraint") <+> pprPred pred
+                   $$
+                   parens (ptext (sLit "Use -XTypeFamilies to permit this"))
 predTyVarErr pred  = sep [ptext (sLit "Non type-variable argument"),
                          nest 2 (ptext (sLit "in the constraint:") <+> pprPred pred)]
 dupPredWarn :: [[PredType]] -> SDoc
@@ -1352,34 +1342,20 @@ compiled elsewhere). In these cases, we let them go through anyway.
 We can also have instances for functions: @instance Foo (a -> b) ...@.
 
 \begin{code}
-checkValidInstHead :: Type -> TcM (Class, [TcType])
-
-checkValidInstHead ty  -- Should be a source type
-  = case tcSplitPredTy_maybe ty of {
-       Nothing -> failWithTc (instTypeErr (ppr ty) empty) ;
-       Just pred -> 
+checkValidInstHead :: Class -> [Type] -> TcM ()
+checkValidInstHead clas tys
+  = do { dflags <- getDOpts
 
-    case getClassPredTys_maybe pred of {
-       Nothing -> failWithTc (instTypeErr (pprPred pred) empty) ;
-        Just (clas,tys) -> do
-
-    dflags <- getDOpts
-    check_inst_head dflags clas tys
-    return (clas, tys)
-    }}
-
-check_inst_head :: DynFlags -> Class -> [Type] -> TcM ()
-check_inst_head dflags clas tys
-  = do { -- If GlasgowExts then check at least one isn't a type variable
+           -- If GlasgowExts then check at least one isn't a type variable
        ; checkTc (xopt Opt_TypeSynonymInstances dflags ||
                   all tcInstHeadTyNotSynonym tys)
-                 (instTypeErr (pprClassPred clas tys) head_type_synonym_msg)
+                 (instTypeErr pp_pred head_type_synonym_msg)
        ; checkTc (xopt Opt_FlexibleInstances dflags ||
                   all tcInstHeadTyAppAllTyVars tys)
-                 (instTypeErr (pprClassPred clas tys) head_type_args_tyvars_msg)
+                 (instTypeErr pp_pred head_type_args_tyvars_msg)
        ; checkTc (xopt Opt_MultiParamTypeClasses dflags ||
                   isSingleton tys)
-                 (instTypeErr (pprClassPred clas tys) head_one_type_msg)
+                 (instTypeErr pp_pred head_one_type_msg)
          -- May not contain type family applications
        ; mapM_ checkTyFamFreeness tys
 
@@ -1392,6 +1368,7 @@ check_inst_head dflags clas tys
        }
 
   where
+    pp_pred = pprClassPred clas tys
     head_type_synonym_msg = parens (
                 text "All instance types must be of the form (T t1 ... tn)" $$
                 text "where T is not a synonym." $$
@@ -1399,7 +1376,7 @@ check_inst_head dflags clas tys
 
     head_type_args_tyvars_msg = parens (vcat [
                 text "All instance types must be of the form (T a1 ... an)",
-                text "where a1 ... an are type *variables*,",
+                text "where a1 ... an are *distinct type variables*,",
                 text "and each type variable appears at most once in the instance head.",
                 text "Use -XFlexibleInstances if you want to disable this."])
 
@@ -1421,35 +1398,30 @@ instTypeErr pp_ty msg
 %************************************************************************
 
 \begin{code}
-checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType -> Type 
-                   -> TcM (Class, [TcType])
-checkValidInstance hs_type tyvars theta tau
+checkValidInstance :: LHsType Name -> [TyVar] -> ThetaType
+                   -> Class -> [TcType] -> TcM ()
+checkValidInstance hs_type tyvars theta clas inst_tys
   = setSrcSpan (getLoc hs_type) $
-    do { (clas, inst_tys) <- setSrcSpan head_loc $
-                              checkValidInstHead tau
-
-        ; undecidable_ok <- xoptM Opt_UndecidableInstances
-
-       ; checkValidTheta InstThetaCtxt theta
+    do  { setSrcSpan head_loc (checkValidInstHead clas inst_tys)
+        ; checkValidTheta InstThetaCtxt theta
        ; checkAmbiguity tyvars theta (tyVarsOfTypes inst_tys)
 
        -- Check that instance inference will terminate (if we care)
        -- For Haskell 98 this will already have been done by checkValidTheta,
         -- but as we may be using other extensions we need to check.
-       ; unless undecidable_ok $
+       ; undecidable_ok <- xoptM Opt_UndecidableInstances
+        ; unless undecidable_ok $
          mapM_ addErrTc (checkInstTermination inst_tys theta)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
-
-        ; return (clas, inst_tys)
-       }
+        }
   where
     msg  = parens (vcat [ptext (sLit "the Coverage Condition fails for one of the functional dependencies;"),
                         undecidableMsg])
 
-       -- The location of the "head" of the instance
+        -- The location of the "head" of the instance
     head_loc = case hs_type of
                  L _ (HsForAllTy _ _ _ (L loc _)) -> loc
                  L loc _                          -> loc