[project @ 2005-03-01 21:40:40 by simonpj]

Type signatures and skolem constants (again)
		Merge to STABLE

This commit lays to rest the vexed question of skolem constants
and type signatures.  My fix last week made type-signature variables
into ordinary meta type variables, because they can be unified
together (see Note [Signature skolems] in TcType).  But that was wrong
becuase GADTs will only refine skolems.

So this commit extends TcTyVarDetails with a new constructors, SigSkolTv,
which is a skolem (like SkolemTv) but is unifiable (like MetaTv).  It's
a bit of a hack, but the code came out quite nicely.

Now the GADT tests work.

diff --git a/ghc/compiler/typecheck/TcBinds.lhs b/ghc/compiler/typecheck/TcBinds.lhs
index a16cddc..c4e1b92 100644 (file)
--- a/ghc/compiler/typecheck/TcBinds.lhs
+++ b/ghc/compiler/typecheck/TcBinds.lhs
@@ -39,7 +39,7 @@ import TcMType                ( newTyFlexiVarTy, zonkQuantifiedTyVar,
 import TcType          ( TcTyVar, SkolemInfo(SigSkol), 
                          TcTauType, TcSigmaType, 
                          mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 
 import TcType          ( TcTyVar, SkolemInfo(SigSkol), 
                          TcTauType, TcSigmaType, 
                          mkTyVarTy, mkForAllTys, mkFunTys, tyVarsOfType, 

-                         mkForAllTy, isUnLiftedType, tcGetTyVar_maybe, 
+                         mkForAllTy, isUnLiftedType, tcGetTyVar, 

                          mkTyVarTys, tidyOpenTyVar, tidyOpenType )
 import Kind            ( argTypeKind )
 import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) 
                          mkTyVarTys, tidyOpenTyVar, tidyOpenType )
 import Kind            ( argTypeKind )
 import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv, emptyTidyEnv ) 

@@ -561,26 +561,7 @@ getMonoBindInfo tc_binds
 %*                                                                     *
 %************************************************************************
 
 %*                                                                     *
 %************************************************************************
 

-Type signatures are tricky.  Consider
-
-  x :: [a]
-  y :: b
-  (x,y,z) = ([y,z], z, head x)
-
-Here, x and y have type sigs, which go into the environment.  We used to
-instantiate their types with skolem constants, and push those types into
-the RHS, so we'd typecheck the RHS with type
-       ( [a*], b*, c )
-where a*, b* are skolem constants, and c is an ordinary meta type varible.
-
-The trouble is that the occurrences of z in the RHS force a* and b* to 
-be the *same*, so we can't make them into skolem constants that don't unify
-with each other.  Alas.
-
-Current solution: don't use skolems at all.  Instead, instantiate the type
-signatures with ordinary meta type variables, and check at the end that
-each group has remained distinct.
-
+Type signatures are tricky.  See Note [Signature skolems] in TcType

 
 \begin{code}
 tcTySigs :: [LSig Name] -> TcM [TcSigInfo]
 
 \begin{code}
 tcTySigs :: [LSig Name] -> TcM [TcSigInfo]

@@ -612,8 +593,10 @@ tcTySig :: LSig Name -> TcM TcSigInfo
 tcTySig (L span (Sig (L _ name) ty))
   = setSrcSpan span            $
     do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty
 tcTySig (L span (Sig (L _ name) ty))
   = setSrcSpan span            $
     do { sigma_ty <- tcHsSigType (FunSigCtxt name) ty

-       ; let rigid_info = SigSkol name
-             poly_id    = mkLocalId name sigma_ty
+       ; (tvs, theta, tau) <- tcInstSigType name sigma_ty
+       ; loc <- getInstLoc (SigOrigin (SigSkol name))
+
+       ; let poly_id = mkLocalId name sigma_ty

 
                -- The scoped names are the ones explicitly mentioned
                -- in the HsForAll.  (There may be more in sigma_ty, because
 
                -- The scoped names are the ones explicitly mentioned
                -- in the HsForAll.  (There may be more in sigma_ty, because

@@ -622,8 +605,6 @@ tcTySig (L span (Sig (L _ name) ty))
                                L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
                                other                      -> []
 
                                L _ (HsForAllTy _ tvs _ _) -> hsLTyVarNames tvs
                                other                      -> []
 

-       ; (tvs, theta, tau) <- tcInstSigType sigma_ty
-       ; loc <- getInstLoc (SigOrigin rigid_info)

        ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
                              sig_loc = loc }) }
        ; return (TcSigInfo { sig_id = poly_id, sig_scoped = scoped_names,
                              sig_tvs = tvs, sig_theta = theta, sig_tau = tau, 
                              sig_loc = loc }) }

@@ -721,26 +702,26 @@ checkDistinctTyVars sig_tvs
        ; return zonked_tvs }
   where
     zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv
        ; return zonked_tvs }
   where
     zonk_one sig_tv = do { ty <- zonkTcTyVar sig_tv

-                        ; case tcGetTyVar_maybe ty of
-                            Just tv' -> return tv'
-                            Nothing  -> bomb_out sig_tv "a type" ty }
+                        ; return (tcGetTyVar "checkDistinctTyVars" ty) }
+       -- 'ty' is bound to be a type variable, because SigSkolTvs
+       -- can only be unified with type variables

 
     check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
        -- The TyVarEnv maps each zonked type variable back to its
        -- corresponding user-written signature type variable
     check_dup acc (sig_tv, zonked_tv)
        = case lookupVarEnv acc zonked_tv of
 
     check_dup :: TyVarEnv TcTyVar -> (TcTyVar, TcTyVar) -> TcM (TyVarEnv TcTyVar)
        -- The TyVarEnv maps each zonked type variable back to its
        -- corresponding user-written signature type variable
     check_dup acc (sig_tv, zonked_tv)
        = case lookupVarEnv acc zonked_tv of

-               Just sig_tv' -> bomb_out sig_tv "another quantified type variable" 
-                                               (mkTyVarTy sig_tv')
+               Just sig_tv' -> bomb_out sig_tv sig_tv'

 
                Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
 
 
                Nothing -> return (extendVarEnv acc zonked_tv sig_tv)
 

-    bomb_out sig_tv doc ty 
-       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv) 
-                    <+> ptext SLIT("is unified with") <+> text doc <+> ppr tidy_ty)
+    bomb_out sig_tv1 sig_tv2
+       = failWithTc (ptext SLIT("Quantified type variable") <+> quotes (ppr tidy_tv1) 
+                    <+> ptext SLIT("is unified with another quantified type variable") 
+                    <+> ppr tidy_tv2)

        where
        where

-        (env1,  tidy_tv) = tidyOpenTyVar emptyTidyEnv sig_tv
-        (_env2, tidy_ty) = tidyOpenType  env1         ty
+        (env1,  tidy_tv1) = tidyOpenTyVar emptyTidyEnv sig_tv1
+        (_env2, tidy_tv2) = tidyOpenTyVar env1         sig_tv2

 \end{code}    
 
 
 \end{code}    
 
 

diff --git a/ghc/compiler/typecheck/TcMType.lhs b/ghc/compiler/typecheck/TcMType.lhs
index f363026..46968f5 100644 (file)
--- a/ghc/compiler/typecheck/TcMType.lhs
+++ b/ghc/compiler/typecheck/TcMType.lhs
@@ -29,7 +29,7 @@ module TcMType (
   Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,
   Rank, UserTypeCtxt(..), checkValidType, pprHsSigCtxt,
   SourceTyCtxt(..), checkValidTheta, checkFreeness,
   checkValidInstHead, instTypeErr, checkAmbiguity,

-  arityErr, isRigidType,
+  arityErr, 

 
   --------------------------------
   -- Zonking
 
   --------------------------------
   -- Zonking

@@ -122,22 +122,6 @@ newTyFlexiVarTy kind
 newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
 newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
 
 newTyFlexiVarTys :: Int -> Kind -> TcM [TcType]
 newTyFlexiVarTys n kind = mappM newTyFlexiVarTy (nOfThem n kind)
 

-isRigidType :: TcType -> TcM Bool
--- Check that the type is rigid, *taking the type refinement into account*
--- In other words if a rigid type variable tv is refined to a wobbly type,
--- the answer should be False
--- ToDo: can this happen?
-isRigidType ty
-  = do { rigids <- mapM is_rigid (varSetElems (tyVarsOfType ty))
-       ; return (and rigids) }
-  where
-    is_rigid tv = do { details <- lookupTcTyVar tv
-                    ; case details of
-                       RigidTv            -> return True
-                       IndirectTv True ty -> isRigidType ty
-                       other              -> return False
-                    }
-

 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
                ; ref <- newMutVar Nothing
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
                ; ref <- newMutVar Nothing

@@ -177,11 +161,9 @@ tcInstTyVars tyvars
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
 
                -- they cannot possibly be captured by
                -- any existing for-alls.  Hence zipTopTvSubst
 

-tcInstTyVar tyvar      -- Use the OccName of the tyvar we are instantiating
-                       -- but make a System Name, so that it's updated in 
-                       -- preference to a tcInstSigTyVar
+tcInstTyVar tyvar      -- Freshen the Name of the tyvar

   = do { uniq <- newUnique
   = do { uniq <- newUnique

-        ; newMetaTyVar (mkSystemName uniq (getOccName tyvar)) 
+        ; newMetaTyVar (setNameUnique (tyVarName tyvar) uniq)

                       (tyVarKind tyvar) Flexi }
 
 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
                       (tyVarKind tyvar) Flexi }
 
 tcInstType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)

@@ -192,25 +174,24 @@ tcInstType ty = tc_inst_type (mappM tcInstTyVar) ty
 
 
 ---------------------------------------------
 
 
 ---------------------------------------------

-tcInstSigType :: TcType -> TcM ([TcTyVar], TcThetaType, TcType)
--- Instantiate a type with fresh meta type variables, but
--- ones which have the same Name as the original type 
--- variable.  This is used for type signatures, where we must
--- instantiate with meta type variables, but we'd like to avoid
--- instantiating them were possible; and the unifier unifies
--- tyvars with System Names by preference
+tcInstSigType :: Name -> TcType -> TcM ([TcTyVar], TcThetaType, TcType)
+-- Instantiate a type with fresh SigSkol variables
+-- See Note [Signature skolems] in TcType.

 -- 
 -- 

+-- Tne new type variables have the sane Name as the original.

 -- We don't need a fresh unique, because the renamer has made them
 -- unique, and it's better not to do so because we extend the envt
 -- with them as scoped type variables, and we'd like to avoid spurious
 -- 's = s' bindings in error messages
 -- We don't need a fresh unique, because the renamer has made them
 -- unique, and it's better not to do so because we extend the envt
 -- with them as scoped type variables, and we'd like to avoid spurious
 -- 's = s' bindings in error messages

-tcInstSigType ty = tc_inst_type tcInstSigTyVars ty
+tcInstSigType id_name ty = tc_inst_type (tcInstSigTyVars id_name) ty

 
 

-tcInstSigTyVars :: [TyVar] -> TcM [TcTyVar]
-tcInstSigTyVars tyvars
+tcInstSigTyVars :: Name -> [TyVar] -> TcM [TcTyVar]
+tcInstSigTyVars id_name tyvars

   = mapM new_tv tyvars
   where
   = mapM new_tv tyvars
   where

-    new_tv tv = newMetaTyVar (tyVarName tv) (tyVarKind tv) Flexi
+    new_tv tv = do { ref <- newMutVar Flexi ;
+                  ; return (mkTcTyVar (tyVarName tv) (tyVarKind tv) 
+                                      (SigSkolTv id_name ref)) }

                            
 
 ---------------------------------------------
                            
 
 ---------------------------------------------

@@ -299,8 +280,7 @@ We return Nothing iff the original box was unbound.
 
 \begin{code}
 data LookupTyVarResult -- The result of a lookupTcTyVar call
 
 \begin{code}
 data LookupTyVarResult -- The result of a lookupTcTyVar call

-  = FlexiTv
-  | RigidTv
+  = DoneTv TcTyVarDetails

   | IndirectTv Bool TcType
        --      True  => This is a non-wobbly type refinement, 
        --               gotten from GADT match unification
   | IndirectTv Bool TcType
        --      True  => This is a non-wobbly type refinement, 
        --               gotten from GADT match unification

@@ -311,31 +291,47 @@ lookupTcTyVar :: TcTyVar -> TcM LookupTyVarResult
 -- This function is the ONLY PLACE that we consult the 
 -- type refinement carried by the monad
 lookupTcTyVar tyvar 
 -- This function is the ONLY PLACE that we consult the 
 -- type refinement carried by the monad
 lookupTcTyVar tyvar 

-  = case tcTyVarDetails tyvar of
+  = let 
+       details =  tcTyVarDetails tyvar
+    in
+    case details of
+      MetaTv ref -> lookup_wobbly details ref
+

       SkolemTv _ -> do { type_reft <- getTypeRefinement
                        ; case lookupVarEnv type_reft tyvar of
                            Just ty -> return (IndirectTv True ty)
       SkolemTv _ -> do { type_reft <- getTypeRefinement
                        ; case lookupVarEnv type_reft tyvar of
                            Just ty -> return (IndirectTv True ty)

-                           Nothing -> return RigidTv
-                       }
-      MetaTv ref -> do         { details <- readMutVar ref
-                       ; case details of
-                           Indirect ty -> return (IndirectTv False ty)
-                           Flexi       -> return FlexiTv
+                           Nothing -> return (DoneTv details)

                        }
 
                        }
 

+       -- For SigSkolTvs try the refinement, and, failing that
+       -- see if it's been unified to anything.  It's a combination
+       -- of SkolemTv and MetaTv
+      SigSkolTv _  ref -> do { type_reft <- getTypeRefinement
+                            ; case lookupVarEnv type_reft tyvar of
+                               Just ty -> return (IndirectTv True ty)
+                               Nothing -> lookup_wobbly details ref
+                            }
+

 -- Look up a meta type variable, conditionally consulting 
 -- the current type refinement
 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
 condLookupTcTyVar use_refinement tyvar 
   | use_refinement = lookupTcTyVar tyvar
   | otherwise
 -- Look up a meta type variable, conditionally consulting 
 -- the current type refinement
 condLookupTcTyVar :: Bool -> TcTyVar -> TcM LookupTyVarResult
 condLookupTcTyVar use_refinement tyvar 
   | use_refinement = lookupTcTyVar tyvar
   | otherwise

-  = case tcTyVarDetails tyvar of
-      SkolemTv _ -> return RigidTv
-      MetaTv ref -> do { details <- readMutVar ref
-                       ; case details of
-                           Indirect ty -> return (IndirectTv False ty)
-                           Flexi       -> return FlexiTv
-                       }
+  = case details of
+      MetaTv ref      -> lookup_wobbly details ref
+      SkolemTv _      -> return (DoneTv details)
+      SigSkolTv _ ref -> lookup_wobbly details ref
+  where 
+    details = tcTyVarDetails tyvar
+
+lookup_wobbly :: TcTyVarDetails -> IORef MetaDetails -> TcM LookupTyVarResult
+lookup_wobbly details ref
+  = do { meta_details <- readMutVar ref
+       ; case meta_details of
+           Indirect ty -> return (IndirectTv False ty)
+           Flexi       -> return (DoneTv details)
+       }

 
 {- 
 -- gaw 2004 We aren't shorting anything out anymore, at least for now
 
 {- 
 -- gaw 2004 We aren't shorting anything out anymore, at least for now

@@ -563,9 +559,9 @@ zonkTyVar unbound_var_fn rflag tyvar
           -- If b is true, the variable was refined, and therefore it is okay
           -- to continue refining inside.  Otherwise it was wobbly and we should
           -- not refine further inside.
           -- If b is true, the variable was refined, and therefore it is okay
           -- to continue refining inside.  Otherwise it was wobbly and we should
           -- not refine further inside.

-         IndirectTv b ty -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
-          FlexiTv         -> unbound_var_fn tyvar         -- Unbound flexi
-          RigidTv         -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary
+         IndirectTv b ty   -> zonkType unbound_var_fn b ty -- Bound flexi/refined rigid
+          DoneTv (MetaTv _) -> unbound_var_fn tyvar        -- Unbound meta type variable
+          DoneTv other      -> return (TyVarTy tyvar)       -- Rigid, no zonking necessary

 \end{code}
 
 
 \end{code}
 
 

diff --git a/ghc/compiler/typecheck/TcPat.lhs b/ghc/compiler/typecheck/TcPat.lhs
index 9261ecb..208af13 100644 (file)
--- a/ghc/compiler/typecheck/TcPat.lhs
+++ b/ghc/compiler/typecheck/TcPat.lhs
@@ -25,7 +25,7 @@ import TcEnv          ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
                          tcLookupClass, tcLookupDataCon, tcLookupId )
 import TcMType                 ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
 import TcType          ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,
                          tcLookupClass, tcLookupDataCon, tcLookupId )
 import TcMType                 ( newTyFlexiVarTy, arityErr, tcSkolTyVars, readMetaTyVar )
 import TcType          ( TcType, TcTyVar, TcSigmaType, TcTauType, zipTopTvSubst,

-                         SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprSkolemTyVar, 
+                         SkolemInfo(PatSkol), isSkolemTyVar, isMetaTyVar, pprTcTyVar, 

                          TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
                          mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
 import VarEnv          ( mkVarEnv )    -- ugly
                          TvSubst, mkOpenTvSubst, substTyVar, substTy, MetaDetails(..),
                          mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy )
 import VarEnv          ( mkVarEnv )    -- ugly

@@ -634,9 +634,7 @@ badTypePat pat = ptext SLIT("Illegal type pattern") <+> ppr pat
 lazyPatErr pat tvs
   = failWithTc $
     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
 lazyPatErr pat tvs
   = failWithTc $
     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))

-       2 (vcat (map get tvs))
-  where
-   get tv = ASSERT( isSkolemTyVar tv ) pprSkolemTyVar tv
+       2 (vcat (map pprTcTyVar tvs))

 
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg

diff --git a/ghc/compiler/typecheck/TcRnTypes.lhs b/ghc/compiler/typecheck/TcRnTypes.lhs
index a89ebf3..33190e7 100644 (file)
--- a/ghc/compiler/typecheck/TcRnTypes.lhs
+++ b/ghc/compiler/typecheck/TcRnTypes.lhs
@@ -50,7 +50,7 @@ import HscTypes               ( FixityEnv,
 import Packages                ( PackageId )
 import Type            ( Type, TvSubstEnv, pprParendType, pprTyThingCategory )
 import TcType          ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo,
 import Packages                ( PackageId )
 import Type            ( Type, TvSubstEnv, pprParendType, pprTyThingCategory )
 import TcType          ( TcTyVarSet, TcType, TcTauType, TcThetaType, SkolemInfo,

-                         TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes )
+                         TcPredType, TcKind, tcCmpPred, tcCmpType, tcCmpTypes, pprSkolInfo )

 import InstEnv         ( DFunId, InstEnv )
 import IOEnv
 import RdrName         ( GlobalRdrEnv, LocalRdrEnv )
 import InstEnv         ( DFunId, InstEnv )
 import IOEnv
 import RdrName         ( GlobalRdrEnv, LocalRdrEnv )

@@ -779,8 +779,6 @@ data InstOrigin
 
 \begin{code}
 pprInstLoc :: InstLoc -> SDoc
 
 \begin{code}
 pprInstLoc :: InstLoc -> SDoc

-pprInstLoc (InstLoc (SigOrigin info) locn _) 
-  = text "arising from" <+> ppr info   -- I don't think this happens much, if at all

 pprInstLoc (InstLoc orig locn _)
   = hsep [text "arising from", pp_orig orig, text "at", ppr locn]
   where
 pprInstLoc (InstLoc orig locn _)
   = hsep [text "arising from", pp_orig orig, text "at", ppr locn]
   where

@@ -791,11 +789,11 @@ pprInstLoc (InstLoc orig locn _)
     pp_orig (LiteralOrigin lit)         = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
     pp_orig (ArithSeqOrigin seq) = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
     pp_orig (PArrSeqOrigin seq)         = hsep [ptext SLIT("the parallel array sequence"), quotes (ppr seq)]
     pp_orig (LiteralOrigin lit)         = hsep [ptext SLIT("the literal"), quotes (ppr lit)]
     pp_orig (ArithSeqOrigin seq) = hsep [ptext SLIT("the arithmetic sequence"), quotes (ppr seq)]
     pp_orig (PArrSeqOrigin seq)         = hsep [ptext SLIT("the parallel array sequence"), quotes (ppr seq)]

-    pp_orig InstSigOrigin       =  ptext SLIT("instantiating a type signature")
-    pp_orig InstScOrigin        =  ptext SLIT("the superclasses of an instance declaration")
+    pp_orig InstSigOrigin       = ptext SLIT("instantiating a type signature")
+    pp_orig InstScOrigin        = ptext SLIT("the superclasses of an instance declaration")

     pp_orig DerivOrigin                 = ptext SLIT("the 'deriving' clause of a data type declaration")
     pp_orig DefaultOrigin       = ptext SLIT("a 'default' declaration")
     pp_orig DerivOrigin                 = ptext SLIT("the 'deriving' clause of a data type declaration")
     pp_orig DefaultOrigin       = ptext SLIT("a 'default' declaration")

-    pp_orig DoOrigin            =  ptext SLIT("a do statement")
-    pp_orig ProcOrigin          =  ptext SLIT("a proc expression")
-    pp_orig (SigOrigin info)    = ppr info
+    pp_orig DoOrigin            = ptext SLIT("a do statement")
+    pp_orig ProcOrigin          = ptext SLIT("a proc expression")
+    pp_orig (SigOrigin info)    = pprSkolInfo info

 \end{code}
 \end{code}

diff --git a/ghc/compiler/typecheck/TcType.lhs b/ghc/compiler/typecheck/TcType.lhs
index ce31dd5..b9ff393 100644 (file)
--- a/ghc/compiler/typecheck/TcType.lhs
+++ b/ghc/compiler/typecheck/TcType.lhs
@@ -23,9 +23,9 @@ module TcType (
   --------------------------------
   -- MetaDetails
   Expected(..), TcRef, TcTyVarDetails(..),
   --------------------------------
   -- MetaDetails
   Expected(..), TcRef, TcTyVarDetails(..),

-  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprSkolemTyVar,
-  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, skolemTvInfo, metaTvRef,
-  isFlexi, isIndirect,
+  MetaDetails(Flexi, Indirect), SkolemInfo(..), pprTcTyVar, pprSkolInfo,
+  isImmutableTyVar, isSkolemTyVar, isMetaTyVar, isExistentialTyVar, metaTvRef,
+  isFlexi, isIndirect, 

 
   --------------------------------
   -- Builders
 
   --------------------------------
   -- Builders

@@ -247,13 +247,45 @@ checking.  It's attached to mutable type variables only.
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 
 It's knot-tied back to Var.lhs.  There is no reason in principle
 why Var.lhs shouldn't actually have the definition, but it "belongs" here.
 

+Note [Signature skolems]
+~~~~~~~~~~~~~~~~~~~~~~~~
+Consider this
+
+  x :: [a]
+  y :: b
+  (x,y,z) = ([y,z], z, head x)
+
+Here, x and y have type sigs, which go into the environment.  We used to
+instantiate their types with skolem constants, and push those types into
+the RHS, so we'd typecheck the RHS with type
+       ( [a*], b*, c )
+where a*, b* are skolem constants, and c is an ordinary meta type varible.
+
+The trouble is that the occurrences of z in the RHS force a* and b* to 
+be the *same*, so we can't make them into skolem constants that don't unify
+with each other.  Alas.
+
+On the other hand, we *must* use skolems for signature type variables, 
+becuase GADT type refinement refines skolems only.  
+
+One solution woudl be insist that in the above defn the programmer uses
+the same type variable in both type signatures.  But that takes explanation.
+
+The alternative (currently implemented) is to have a special kind of skolem
+constant, SigSkokTv, which can unify with other SigSkolTvs.  
+
+

 \begin{code}
 type TcTyVar = TyVar   -- Used only during type inference
 
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails
 \begin{code}
 type TcTyVar = TyVar   -- Used only during type inference
 
 -- A TyVarDetails is inside a TyVar
 data TcTyVarDetails

-  = SkolemTv SkolemInfo                -- A skolem constant
-  | MetaTv (IORef MetaDetails) -- A meta type variable stands for a tau-type
+  = MetaTv (IORef MetaDetails)         -- A meta type variable stands for a tau-type
+  | SkolemTv SkolemInfo                        -- A skolem constant
+  | SigSkolTv Name (IORef MetaDetails) -- Ditto, but from a type signature;
+                                       --      see Note [Signature skolems]
+                                       --      The MetaDetails, if filled in, will 
+                                       --      always be another SigSkolTv

 
 data SkolemInfo
   = SigSkol Name       -- Bound at a type signature
 
 data SkolemInfo
   = SigSkol Name       -- Bound at a type signature

@@ -282,30 +314,34 @@ tidySkolemTyVar :: TidyEnv -> TcTyVar -> (TidyEnv, TcTyVar)
 -- Tidy the type inside a GenSkol, preparatory to printing it
 tidySkolemTyVar env tv
   = ASSERT( isSkolemTyVar tv )
 -- Tidy the type inside a GenSkol, preparatory to printing it
 tidySkolemTyVar env tv
   = ASSERT( isSkolemTyVar tv )

-    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) (SkolemTv info1))
+    (env1, mkTcTyVar (tyVarName tv) (tyVarKind tv) info1)

   where
   where

-    (env1, info1) = case skolemTvInfo tv of
-                     GenSkol tvs ty loc -> (env2, GenSkol tvs1 ty1 loc)
+    (env1, info1) = case tcTyVarDetails tv of
+                     SkolemTv (GenSkol tvs ty loc) -> (env2, SkolemTv (GenSkol tvs1 ty1 loc))

                            where
                              (env1, tvs1) = tidyOpenTyVars env tvs
                              (env2, ty1)  = tidyOpenType env1 ty
                      info -> (env, info)
                     
                            where
                              (env1, tvs1) = tidyOpenTyVars env tvs
                              (env2, ty1)  = tidyOpenType env1 ty
                      info -> (env, info)
                     

-pprSkolemTyVar :: TcTyVar -> SDoc
-pprSkolemTyVar tv
-  = ASSERT( isSkolemTyVar tv )
-    quotes (ppr tv) <+> ptext SLIT("is bound by") <+> ppr (skolemTvInfo tv)
-
-instance Outputable SkolemInfo where
-  ppr (SigSkol id)  = ptext SLIT("the type signature for") <+> quotes (ppr id)
-  ppr (ClsSkol cls) = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
-  ppr (InstSkol df) = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
-  ppr (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
-  ppr (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
-                           nest 2 (ptext SLIT("at") <+> ppr loc)]
-  ppr (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
-                                 <+> quotes (ppr (mkForAllTys tvs ty)),
-                                 nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprTcTyVar :: TcTyVar -> SDoc
+-- Print tyvar with info about its binding
+pprTcTyVar tv
+  = quotes (ppr tv) <+> ppr_details (tcTyVarDetails tv)
+  where
+    ppr_details (MetaTv _)      = ptext SLIT("is a meta type variable")
+    ppr_details (SigSkolTv id _) = ptext SLIT("is bound by") <+> pprSkolInfo (SigSkol id)
+    ppr_details (SkolemTv info)  = ptext SLIT("is bound by") <+> pprSkolInfo info
+ 
+pprSkolInfo :: SkolemInfo -> SDoc
+pprSkolInfo (SigSkol id)     = ptext SLIT("the type signature for") <+> quotes (ppr id)
+pprSkolInfo (ClsSkol cls)    = ptext SLIT("the class declaration for") <+> quotes (ppr cls)
+pprSkolInfo (InstSkol df)    = ptext SLIT("the instance declaration at") <+> ppr (getSrcLoc df)
+pprSkolInfo (ArrowSkol loc)  = ptext SLIT("the arrow form at") <+> ppr loc
+pprSkolInfo (PatSkol dc loc) = sep [ptext SLIT("the pattern for") <+> quotes (ppr dc),
+                                   nest 2 (ptext SLIT("at") <+> ppr loc)]
+pprSkolInfo (GenSkol tvs ty loc) = sep [ptext SLIT("the polymorphic type") 
+                                       <+> quotes (ppr (mkForAllTys tvs ty)),
+                                       nest 2 (ptext SLIT("at") <+> ppr loc)]

 
 instance Outputable MetaDetails where
   ppr Flexi        = ptext SLIT("Flexi")
 
 instance Outputable MetaDetails where
   ppr Flexi        = ptext SLIT("Flexi")

@@ -319,8 +355,9 @@ isImmutableTyVar tv
 isSkolemTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
 isSkolemTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of

-       SkolemTv _ -> True
-       MetaTv _   -> False
+       SkolemTv _    -> True
+       SigSkolTv _ _ -> True
+       MetaTv _      -> False

 
 isExistentialTyVar tv  -- Existential type variable, bound by a pattern
   = ASSERT( isTcTyVar tv )
 
 isExistentialTyVar tv  -- Existential type variable, bound by a pattern
   = ASSERT( isTcTyVar tv )

@@ -331,20 +368,15 @@ isExistentialTyVar tv     -- Existential type variable, bound by a pattern
 isMetaTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
 isMetaTyVar tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of

-       SkolemTv _ -> False

        MetaTv _   -> True
        MetaTv _   -> True

-
-skolemTvInfo :: TyVar -> SkolemInfo
-skolemTvInfo tv 
-  = ASSERT( isTcTyVar tv )
-    case tcTyVarDetails tv of
-       SkolemTv info -> info
+       other      -> False

 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of
 
 metaTvRef :: TyVar -> IORef MetaDetails
 metaTvRef tv 
   = ASSERT( isTcTyVar tv )
     case tcTyVarDetails tv of

-        MetaTv ref -> ref
+       MetaTv ref -> ref
+       other      -> pprPanic "metaTvRef" (ppr tv)

 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True
 
 isFlexi, isIndirect :: MetaDetails -> Bool
 isFlexi Flexi = True

diff --git a/ghc/compiler/typecheck/TcUnify.lhs b/ghc/compiler/typecheck/TcUnify.lhs
index 395df1e..85f4eb9 100644 (file)
--- a/ghc/compiler/typecheck/TcUnify.lhs
+++ b/ghc/compiler/typecheck/TcUnify.lhs
@@ -34,9 +34,9 @@ import TypeRep                ( Type(..), PredType(..), TyNote(..) )
 
 import TcRnMonad         -- TcType, amongst others
 import TcType          ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,
 
 import TcRnMonad         -- TcType, amongst others
 import TcType          ( TcKind, TcType, TcSigmaType, TcRhoType, TcTyVar, TcTauType,

-                         TcTyVarSet, TcThetaType, Expected(..), 
+                         TcTyVarSet, TcThetaType, Expected(..), TcTyVarDetails(..),

                          SkolemInfo( GenSkol ), MetaDetails(..), 
                          SkolemInfo( GenSkol ), MetaDetails(..), 

-                         pprSkolemTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,
+                         pprTcTyVar, isTauTy, isSigmaTy, mkFunTys, mkTyConApp,

                          tcSplitAppTy_maybe, tcSplitTyConApp_maybe, 
                          tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,
                          tcSplitAppTy_maybe, tcSplitTyConApp_maybe, 
                          tyVarsOfType, mkPhiTy, mkTyVarTy, mkPredTy,
                          typeKind, tcSplitFunTy_maybe, mkForAllTys, mkAppTy,

@@ -48,7 +48,7 @@ import Kind           ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
                          isSubKind, pprKind, splitKindFunTys )
 import Inst            ( newDicts, instToId, tcInstCall )
 import TcMType         ( condLookupTcTyVar, LookupTyVarResult(..),
                          isSubKind, pprKind, splitKindFunTys )
 import Inst            ( newDicts, instToId, tcInstCall )
 import TcMType         ( condLookupTcTyVar, LookupTyVarResult(..),

-                          putMetaTyVar, tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,
+                          tcSkolType, newKindVar, tcInstTyVars, newMetaTyVar,

                          newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV, 
                          readKindVar, writeKindVar )
 import TcSimplify      ( tcSimplifyCheck )
                          newTyFlexiVarTy, zonkTcKind, zonkType, zonkTcType,  zonkTcTyVarsAndFV, 
                          readKindVar, writeKindVar )
 import TcSimplify      ( tcSimplifyCheck )

@@ -827,31 +827,57 @@ uVar swapped r1 tv1 r2 ps_ty2 ty2
     case details of
        IndirectTv r1' ty1 | swapped   -> uTys r2   ps_ty2 ty2 r1' ty1    ty1   -- Swap back
                           | otherwise -> uTys r1' ty1     ty1 r2  ps_ty2 ty2   -- Same order
     case details of
        IndirectTv r1' ty1 | swapped   -> uTys r2   ps_ty2 ty2 r1' ty1    ty1   -- Swap back
                           | otherwise -> uTys r1' ty1     ty1 r2  ps_ty2 ty2   -- Same order

-       FlexiTv -> uFlexiVar swapped tv1 r2 ps_ty2 ty2
-       RigidTv -> uRigidVar swapped tv1 r2 ps_ty2 ty2
-
-       -- Expand synonyms; ignore FTVs
-uFlexiVar :: Bool -> TcTyVar -> 
-             Bool ->   -- Allow refinements to ty2
-             TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Flexi
-uFlexiVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
-  = uFlexiVar swapped tv1 r2 ps_ty2 ty2
-
-uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
+       DoneTv details1 -> uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+----------------
+uDoneVar :: Bool                       -- Args are swapped
+        -> TcTyVar -> TcTyVarDetails   -- Tyvar 1
+        -> Bool                        -- Allow refinements to ty2
+        -> TcTauType -> TcTauType      -- Type 2
+        -> TcM ()
+-- Invariant: tyvar 1 is not unified with anything
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 (NoteTy n2 ty2)
+  =    -- Expand synonyms; ignore FTVs
+    uDoneVar swapped tv1 details1 r2 ps_ty2 ty2
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 ty2@(TyVarTy tv2)

        -- Same type variable => no-op
   | tv1 == tv2
   = returnM ()
 
        -- Distinct type variables
   | otherwise
        -- Same type variable => no-op
   | tv1 == tv2
   = returnM ()
 
        -- Distinct type variables
   | otherwise

-  = condLookupTcTyVar r2 tv2   `thenM` \ details ->
-    case details of
-       IndirectTv b ty2'    -> uFlexiVar swapped tv1 b ty2' ty2'
-       FlexiTv | update_tv2 -> putMetaTyVar tv2 (TyVarTy tv1)
-               | otherwise  -> updateFlexi swapped tv1 ty2
-       RigidTv              -> updateFlexi swapped tv1 ty2
-       -- Note that updateFlexi does a sub-kind check
+  = do { lookup2 <- condLookupTcTyVar r2 tv2
+       ; case lookup2 of
+               IndirectTv b ty2' -> uDoneVar  swapped tv1 details1 b ty2' ty2'
+               DoneTv details2   -> uDoneVars swapped tv1 details1 tv2 details2
+       }
+
+uDoneVar swapped tv1 details1 r2 ps_ty2 non_var_ty2    -- ty2 is not a type variable
+  = case details1 of
+       MetaTv ref1 -> do {     -- Do the occurs check, and check that we are not
+                               -- unifying a type variable with a polytype
+                               -- Returns a zonked type ready for the update
+                           ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
+                         ; updateMeta swapped tv1 ref1 ty2 }
+
+       skolem_details -> unifyMisMatch (TyVarTy tv1) ps_ty2
+
+
+----------------
+uDoneVars :: Bool                      -- Args are swapped
+         -> TcTyVar -> TcTyVarDetails  -- Tyvar 1
+         -> TcTyVar -> TcTyVarDetails  -- Tyvar 2
+         -> TcM ()
+-- Invarant: the type variables are distinct, 
+-- and are not already unified with anything
+
+uDoneVars swapped tv1 (MetaTv ref1) tv2 details2
+  = case details2 of
+       MetaTv ref2 | update_tv2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+       other                    -> updateMeta swapped       tv1 ref1 (mkTyVarTy tv2)
+       -- Note that updateMeta does a sub-kind check

        -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
   where
     k1 = tyVarKind tv1
        -- We might unify (a b) with (c d) where b::*->* and d::*; this should fail
   where
     k1 = tyVarKind tv1

@@ -863,46 +889,27 @@ uFlexiVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
        -- so we can choose which to do.
 
     nicer_to_update_tv2 = isSystemName (varName tv2)
        -- so we can choose which to do.
 
     nicer_to_update_tv2 = isSystemName (varName tv2)

-       -- Try to update sys-y type variables in preference to sig-y ones
-
-  -- First one is flexi, second one isn't a type variable
-uFlexiVar swapped tv1 r2 ps_ty2 non_var_ty2
-  =    -- Do the occurs check, and check that we are not
-       -- unifying a type variable with a polytype
-       -- Returns a zonked type ready for the update
-    do { ty2 <- checkValue tv1 r2 ps_ty2 non_var_ty2
-       ; updateFlexi swapped tv1 ty2 }
-
--- Ready to update tv1, which is flexi; occurs check is done
-updateFlexi swapped tv1 ty2
-  = do { checkKinds swapped tv1 ty2
-       ; putMetaTyVar tv1 ty2 }
-
-
-uRigidVar :: Bool -> TcTyVar
-          -> Bool -> -- Allow refinements to ty2
-             TcTauType -> TcTauType -> TcM ()
--- Invariant: tv1 is Rigid
-uRigidVar swapped tv1 r2 ps_ty2 (NoteTy n2 ty2)
-  = uRigidVar swapped tv1 r2 ps_ty2 ty2
+       -- Try to update sys-y type variables in preference to ones
+       -- gotten (say) by instantiating a polymorphic function with
+       -- a user-written type sig
+       
+uDoneVars swapped tv1 (SkolemTv _) tv2 details2
+  = case details2 of
+       MetaTv ref2 -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+       other       -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)

 
 

-       -- The both-type-variable case
-uRigidVar swapped tv1 r2 ps_ty2 ty2@(TyVarTy tv2)
-       -- Same type variable => no-op
-  | tv1 == tv2
-  = returnM ()
+uDoneVars swapped tv1 (SigSkolTv _ ref1) tv2 details2
+  = case details2 of
+       MetaTv ref2   -> updateMeta (not swapped) tv2 ref2 (mkTyVarTy tv1)
+       SigSkolTv _ _ -> updateMeta swapped tv1 ref1 (mkTyVarTy tv2)
+       other         -> unifyMisMatch (mkTyVarTy tv1) (mkTyVarTy tv2)

 
 

-       -- Distinct type variables
-  | otherwise
-  = condLookupTcTyVar r2 tv2   `thenM` \ details ->
-    case details of
-       IndirectTv b ty2' -> uRigidVar swapped tv1 b ty2' ty2'
-       FlexiTv -> updateFlexi swapped tv2 (TyVarTy tv1)
-       RigidTv -> unifyMisMatch (TyVarTy tv1) (TyVarTy tv2) 
-
-       -- Second one isn't a type variable
-uRigidVar swapped tv1 r2 ps_ty2 non_var_ty2
-  = unifyMisMatch (TyVarTy tv1) ps_ty2
+----------------
+updateMeta :: Bool -> TcTyVar -> IORef MetaDetails -> TcType -> TcM ()
+-- Update tv1, which is flexi; occurs check is alrady done
+updateMeta swapped tv1 ref1 ty2
+  = do { checkKinds swapped tv1 ty2
+       ; writeMutVar ref1 (Indirect ty2) }

 \end{code}
 
 \begin{code}
 \end{code}
 
 \begin{code}

@@ -919,7 +926,6 @@ checkKinds swapped tv1 ty2
        --      unlifted type: e.g.  (id 3#) is illegal
   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2)        $
     unifyKindMisMatch k1 k2
        --      unlifted type: e.g.  (id 3#) is illegal
   = addErrCtxtM (unifyKindCtxt swapped tv1 ty2)        $
     unifyKindMisMatch k1 k2

-

   where
     (k1,k2) | swapped   = (tk2,tk1)
            | otherwise = (tk1,tk2)
   where
     (k1,k2) | swapped   = (tk2,tk1)
            | otherwise = (tk1,tk2)

@@ -1186,7 +1192,7 @@ ppr_ty env ty
        ; case tidy_ty of
           TyVarTy tv 
                | isSkolemTyVar tv -> return (env2, pp_rigid tv',
        ; case tidy_ty of
           TyVarTy tv 
                | isSkolemTyVar tv -> return (env2, pp_rigid tv',

-                                             pprSkolemTyVar tv')
+                                             pprTcTyVar tv')

                | otherwise -> return simple_result
                where
                  (env2, tv') = tidySkolemTyVar env1 tv
                | otherwise -> return simple_result
                where
                  (env2, tv') = tidySkolemTyVar env1 tv