Use implication constraints to improve type inference
[ghc-hetmet.git] / compiler / typecheck / TcMType.lhs
index f01d69d..4a12536 100644 (file)
@@ -1,9 +1,12 @@
 %
+% (c) The University of Glasgow 2006
 % (c) The GRASP/AQUA Project, Glasgow University, 1992-1998
 %
-\section{Monadic type operations}
 
-This module contains monadic operations over types that contain mutable type variables
+Monadic type operations
+
+This module contains monadic operations over types that contain
+mutable type variables
 
 \begin{code}
 module TcMType (
@@ -46,7 +49,7 @@ module TcMType (
   zonkType, zonkTcPredType, 
   zonkTcTyVar, zonkTcTyVars, zonkTcTyVarsAndFV, zonkQuantifiedTyVar,
   zonkTcType, zonkTcTypes, zonkTcClassConstraints, zonkTcThetaType,
-  zonkTcKindToKind, zonkTcKind,
+  zonkTcKindToKind, zonkTcKind, zonkTopTyVar,
 
   readKindVar, writeKindVar
 
@@ -54,60 +57,32 @@ module TcMType (
 
 #include "HsVersions.h"
 
-
 -- friends:
-import TypeRep         ( Type(..), PredType(..),  -- Friend; can see representation
-                         ThetaType
-                       ) 
-import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
-                         TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
-                         MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
-                         BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef,
-                         mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef,
-                         tcCmpPred, isClassPred, tcGetTyVar,
-                         tcSplitPhiTy, tcSplitPredTy_maybe,
-                         tcSplitAppTy_maybe,  
-                         tcValidInstHeadTy, tcSplitForAllTys,
-                         tcIsTyVarTy, tcSplitSigmaTy, 
-                         isUnLiftedType, isIPPred, 
-                         typeKind, isSkolemTyVar,
-                         mkAppTy, mkTyVarTy, mkTyVarTys, 
-                         tyVarsOfPred, getClassPredTys_maybe,
-                         tyVarsOfType, tyVarsOfTypes, tcView,
-                         pprPred, pprTheta, pprClassPred )
-import Type            ( Kind, KindVar, 
-                         isLiftedTypeKind, isSubArgTypeKind, isSubOpenTypeKind,
-                         liftedTypeKind, defaultKind
-                       )
-import Type            ( TvSubst, zipTopTvSubst, substTy )
-import Coercion                ( mkCoKind )
-import Class           ( Class, classArity, className )
-import TyCon           ( TyCon, isSynTyCon, isUnboxedTupleTyCon, 
-                         tyConArity, tyConName )
-import Var             ( TyVar, tyVarKind, tyVarName, isTcTyVar, 
-                         mkTyVar, mkTcTyVar, tcTyVarDetails,
-                         CoVar, mkCoVar )
-
-       -- Assertions
-#ifdef DEBUG
-import TcType          ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Type            ( isSubKind )
-#endif
+import TypeRep
+import TcType
+import Type
+import Type
+import Coercion
+import Class
+import TyCon
+import Var
 
 -- others:
 import TcRnMonad          -- TcType, amongst others
-import FunDeps         ( grow, checkInstCoverage )
-import Name            ( Name, setNameUnique, mkSysTvName )
+import FunDeps
+import Name
 import VarSet
-import DynFlags                ( dopt, DynFlag(..) )
-import Util            ( nOfThem, isSingleton, notNull )
-import ListSetOps      ( removeDups )
-import UniqSupply      ( uniqsFromSupply )
+import ErrUtils
+import DynFlags
+import Util
+import Maybes
+import ListSetOps
+import UniqSupply
+import SrcLoc
 import Outputable
 
 import Control.Monad   ( when )
 import Data.List       ( (\\) )
-
 \end{code}
 
 
@@ -186,19 +161,30 @@ tcSkolSigTyVars :: SkolemInfo -> [TyVar] -> [TcTyVar]
 tcSkolSigTyVars info tyvars = [ mkSkolTyVar (tyVarName tv) (tyVarKind tv) info
                              | tv <- tyvars ]
 
-tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh skolem constants
-tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
-
-tcInstSkolTyVar :: SkolemInfo -> TyVar -> TcM TcTyVar
-tcInstSkolTyVar info tyvar
+tcInstSkolTyVar :: SkolemInfo -> Maybe SrcLoc -> TyVar -> TcM TcTyVar
+-- Instantiate the tyvar, using 
+--     * the occ-name and kind of the supplied tyvar, 
+--     * the unique from the monad,
+--     * the location either from the tyvar (mb_loc = Nothing)
+--       or from mb_loc (Just loc)
+tcInstSkolTyVar info mb_loc tyvar
   = do { uniq <- newUnique
-       ; let name = setNameUnique (tyVarName tyvar) uniq
-             kind = tyVarKind tyvar
-       ; return (mkSkolTyVar name kind info) }
+       ; let old_name = tyVarName tyvar
+             kind     = tyVarKind tyvar
+             loc      = mb_loc `orElse` getSrcLoc old_name
+             new_name = mkInternalName uniq (nameOccName old_name) loc
+       ; return (mkSkolTyVar new_name kind info) }
 
 tcInstSkolTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
-tcInstSkolTyVars info tyvars = mapM (tcInstSkolTyVar info) tyvars
+-- Get the location from the monad
+tcInstSkolTyVars info tyvars 
+  = do         { span <- getSrcSpanM
+       ; mapM (tcInstSkolTyVar info (Just (srcSpanStart span))) tyvars }
+
+tcInstSkolType :: SkolemInfo -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh skolem constants
+-- Binding location comes from the monad
+tcInstSkolType info ty = tcInstType (tcInstSkolTyVars info) ty
 \end{code}
 
 
@@ -301,9 +287,14 @@ tcInstTyVars tyvars
 %************************************************************************
 
 \begin{code}
-tcInstSigTyVars :: SkolemInfo -> [TyVar] -> TcM [TcTyVar]
--- Instantiate with meta SigTvs
-tcInstSigTyVars skol_info tyvars 
+tcInstSigTyVars :: Bool -> SkolemInfo -> [TyVar] -> TcM [TcTyVar]
+-- Instantiate with skolems or meta SigTvs; depending on use_skols
+-- Always take location info from the supplied tyvars
+tcInstSigTyVars use_skols skol_info tyvars 
+  | use_skols
+  = mapM (tcInstSkolTyVar skol_info Nothing) tyvars
+
+  | otherwise
   = mapM (instMetaTyVar (SigTv skol_info)) tyvars
 
 zonkSigTyVar :: TcTyVar -> TcM TcTyVar
@@ -469,6 +460,30 @@ zonkTcPredType (EqPred t1 t2)
                     are used at the end of type checking
 
 \begin{code}
+zonkTopTyVar :: TcTyVar -> TcM TcTyVar
+-- zonkTopTyVar is used, at the top level, on any un-instantiated meta type variables
+-- to default the kind of ? and ?? etc to *.  This is important to ensure that
+-- instance declarations match.  For example consider
+--     instance Show (a->b)
+--     foo x = show (\_ -> True)
+-- Then we'll get a constraint (Show (p ->q)) where p has argTypeKind (printed ??), 
+-- and that won't match the typeKind (*) in the instance decl.
+--
+-- Because we are at top level, no further constraints are going to affect these
+-- type variables, so it's time to do it by hand.  However we aren't ready
+-- to default them fully to () or whatever, because the type-class defaulting
+-- rules have yet to run.
+
+zonkTopTyVar tv
+  | k `eqKind` default_k = return tv
+  | otherwise
+  = do { tv' <- newFlexiTyVar default_k
+       ; writeMetaTyVar tv (mkTyVarTy tv') 
+       ; return tv' }
+  where
+    k = tyVarKind tv
+    default_k = defaultKind k
+
 zonkQuantifiedTyVar :: TcTyVar -> TcM TyVar
 -- zonkQuantifiedTyVar is applied to the a TcTyVar when quantifying over it.
 -- It might be a meta TyVar, in which case we freeze it into an ordinary TyVar.
@@ -688,7 +703,6 @@ checkValidType ctxt ty
                 ConArgCtxt _   -> Rank 1       -- We are given the type of the entire
                                                -- constructor, hence rank 1
                 ForSigCtxt _   -> Rank 1
-                RuleSigCtxt _  -> Rank 1
                 SpecInstCtxt   -> Rank 1
 
        actual_kind = typeKind ty
@@ -1014,7 +1028,9 @@ even in a scope where b is in scope.
 
 \begin{code}
 checkFreeness forall_tyvars theta
-  = mappM_ complain (filter is_free theta)
+  = do { gla_exts <- doptM Opt_GlasgowExts
+       ; if gla_exts then return ()    -- New!  Oct06
+         else mappM_ complain (filter is_free theta) }
   where    
     is_free pred     =  not (isIPPred pred)
                     && not (any bound_var (varSetElems (tyVarsOfPred pred)))
@@ -1130,14 +1146,15 @@ 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) $
-              checkInstTermination theta inst_tys
+         mapM_ failWithTc (checkInstTermination inst_tys theta)
        
        -- The Coverage Condition
        ; checkTc (undecidable_ok || checkInstCoverage clas inst_tys)
                  (instTypeErr (pprClassPred clas inst_tys) msg)
        }
   where
-    msg  = parens (ptext SLIT("the Coverage Condition fails for one of the functional dependencies"))
+    msg  = parens (vcat [ptext SLIT("the Coverage Condition fails for one of the functional dependencies;"),
+                        undecidableMsg])
 \end{code}
 
 Termination test: each assertion in the context satisfies
@@ -1154,20 +1171,19 @@ The underlying idea is that
 
 
 \begin{code}
-checkInstTermination :: ThetaType -> [TcType] -> TcM ()
-checkInstTermination theta tys
-  = do { mappM_ (check_nomore (fvTypes tys))    theta
-       ; mappM_ (check_smaller (sizeTypes tys)) theta }
-
-check_nomore :: [TyVar] -> PredType -> TcM ()
-check_nomore fvs pred
-  = checkTc (null (fvPred pred \\ fvs))
-           (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
-
-check_smaller :: Int -> PredType -> TcM ()
-check_smaller n pred
-  = checkTc (sizePred pred < n)
-           (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+checkInstTermination :: [TcType] -> ThetaType -> [Message]
+checkInstTermination tys theta
+  = mapCatMaybes check theta
+  where
+   fvs  = fvTypes tys
+   size = sizeTypes tys
+   check pred 
+      | not (null (fvPred pred \\ fvs)) 
+      = Just (predUndecErr pred nomoreMsg $$ parens undecidableMsg)
+      | sizePred pred >= size
+      = Just (predUndecErr pred smallerMsg $$ parens undecidableMsg)
+      | otherwise
+      = Nothing
 
 predUndecErr pred msg = sep [msg,
                        nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]