Massive patch for the first months work adding System FC to GHC #34
authorManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 20 Sep 2006 16:49:16 +0000 (16:49 +0000)
committerManuel M T Chakravarty <chak@cse.unsw.edu.au>
Wed, 20 Sep 2006 16:49:16 +0000 (16:49 +0000)
Fri Sep 15 18:56:58 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
  * Massive patch for the first months work adding System FC to GHC #34
  Fri Aug  4 18:20:57 EDT 2006  Manuel M T Chakravarty <chak@cse.unsw.edu.au>
    * Massive patch for the first months work adding System FC to GHC #34

    Broken up massive patch -=chak
    Original log message:
    This is (sadly) all done in one patch to avoid Darcs bugs.
    It's not complete work... more FC stuff to come.  A compiler
    using just this patch will fail dismally.

20 files changed:
compiler/typecheck/Inst.lhs
compiler/typecheck/TcArrows.lhs
compiler/typecheck/TcBinds.lhs
compiler/typecheck/TcDeriv.lhs
compiler/typecheck/TcEnv.lhs
compiler/typecheck/TcExpr.lhs
compiler/typecheck/TcHsSyn.lhs
compiler/typecheck/TcHsType.lhs
compiler/typecheck/TcMType.lhs
compiler/typecheck/TcMatches.lhs
compiler/typecheck/TcPat.lhs
compiler/typecheck/TcRnDriver.lhs
compiler/typecheck/TcRnMonad.lhs
compiler/typecheck/TcRnTypes.lhs
compiler/typecheck/TcSimplify.lhs
compiler/typecheck/TcSplice.lhs
compiler/typecheck/TcTyClsDecls.lhs
compiler/typecheck/TcType.lhs
compiler/typecheck/TcType.lhs-boot
compiler/typecheck/TcUnify.lhs

index 77ca56a..8971320 100644 (file)
@@ -12,7 +12,7 @@ module Inst (
 
        tidyInsts, tidyMoreInsts,
 
-       newDicts, newDictAtLoc, newDictsAtLoc, cloneDict, 
+       newDicts, newDictsAtLoc, cloneDict, 
        shortCutFracLit, shortCutIntLit, newIPDict, 
        newMethod, newMethodFromName, newMethodWithGivenTy, 
        tcInstClassOp, tcInstStupidTheta,
@@ -22,6 +22,7 @@ module Inst (
        ipNamesOfInst, ipNamesOfInsts, fdPredsOfInst, fdPredsOfInsts,
        instLoc, getDictClassTys, dictPred,
 
+       mkInstCoFn, 
        lookupInst, LookupInstResult(..), lookupPred, 
        tcExtendLocalInstEnv, tcGetInstEnvs, getOverlapFlag,
 
@@ -30,7 +31,7 @@ module Inst (
        isTyVarDict, isMethodFor, 
 
        zonkInst, zonkInsts,
-       instToId, instName,
+       instToId, instToVar, instName,
 
        InstOrigin(..), InstLoc(..), pprInstLoc
     ) where
@@ -40,8 +41,8 @@ module Inst (
 import {-# SOURCE #-}  TcExpr( tcPolyExpr )
 
 import HsSyn   ( HsLit(..), HsOverLit(..), HsExpr(..), LHsExpr, mkHsApp,
-                 nlHsLit, nlHsVar )
-import TcHsSyn ( mkHsTyApp, mkHsDictApp, zonkId )
+                 ExprCoFn(..), (<.>), nlHsLit, nlHsVar )
+import TcHsSyn ( zonkId )
 import TcRnMonad
 import TcEnv   ( tcLookupId, checkWellStaged, topIdLvl, tcMetaTy )
 import InstEnv ( DFunId, InstEnv, Instance(..), OverlapFlag(..),
@@ -69,10 +70,11 @@ import Type ( TvSubst, substTy, substTyVar, substTyWith, substTheta, zipTopTvSub
                  notElemTvSubst, extendTvSubstList )
 import Unify   ( tcMatchTys )
 import Module  ( modulePackageId )
-import Kind    ( isSubKind )
+import {- Kind parts of -} Type        ( isSubKind )
 import HscTypes        ( ExternalPackageState(..), HscEnv(..) )
 import CoreFVs ( idFreeTyVars )
-import DataCon ( DataCon, dataConTyVars, dataConStupidTheta, dataConName, dataConWrapId )
+import DataCon ( DataCon, dataConStupidTheta, dataConName, 
+                  dataConWrapId, dataConUnivTyVars )
 import Id      ( Id, idName, idType, mkUserLocal, mkLocalId )
 import Name    ( Name, mkMethodOcc, getOccName, getSrcLoc, nameModule,
                  isInternalName, setNameUnique )
@@ -95,13 +97,23 @@ import Outputable
 Selection
 ~~~~~~~~~
 \begin{code}
+mkInstCoFn :: [TcType] -> [Inst] -> ExprCoFn
+mkInstCoFn tys dicts = CoApps (map instToId dicts) <.> CoTyApps tys
+
 instName :: Inst -> Name
 instName inst = idName (instToId inst)
 
 instToId :: Inst -> TcId
-instToId (LitInst nm _ ty _) = mkLocalId nm ty
-instToId (Dict nm pred _)    = mkLocalId nm (mkPredTy pred)
-instToId (Method id _ _ _ _) = id
+instToId inst = ASSERT2( isId id, ppr inst ) id 
+             where
+               id = instToVar inst
+
+instToVar :: Inst -> Var
+instToVar (LitInst nm _ ty _) = mkLocalId nm ty
+instToVar (Method id _ _ _ _) = id
+instToVar (Dict nm pred _)    
+  | isEqPred pred = mkTyVar nm (mkPredTy pred)
+  | otherwise    = mkLocalId nm (mkPredTy pred)
 
 instLoc (Dict _ _       loc) = loc
 instLoc (Method _ _ _ _ loc) = loc
@@ -207,29 +219,28 @@ newDicts orig theta
   = getInstLoc orig            `thenM` \ loc ->
     newDictsAtLoc loc theta
 
-cloneDict :: Inst -> TcM Inst
+cloneDict :: Inst -> TcM Inst  -- Only used for linear implicit params
 cloneDict (Dict nm ty loc) = newUnique `thenM` \ uniq ->
                             returnM (Dict (setNameUnique nm uniq) ty loc)
 
-newDictAtLoc :: InstLoc -> TcPredType -> TcM Inst
-newDictAtLoc inst_loc pred
-  = do { uniq <- newUnique
-       ; return (mkDict inst_loc uniq pred) }
-
 newDictsAtLoc :: InstLoc -> TcThetaType -> TcM [Inst]
-newDictsAtLoc inst_loc theta
-  = newUniqueSupply            `thenM` \ us ->
-    returnM (zipWith (mkDict inst_loc) (uniqsFromSupply us) theta)
-
-mkDict inst_loc uniq pred
-  = Dict name pred inst_loc
-  where
-    name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
+newDictsAtLoc inst_loc theta = mapM (newDictAtLoc inst_loc) theta
+
+{-
+newDictOcc :: InstLoc -> TcPredType -> TcM Inst
+newDictOcc inst_loc (EqPred ty1 ty2)
+  = do { unifyType ty1 ty2     -- We insist that they unify right away
+       ; return ty1 }          -- And return the relexive coercion
+-}
+newDictAtLoc inst_loc pred
+  = do         { uniq <- newUnique 
+       ; let name = mkPredName uniq (instLocSrcLoc inst_loc) pred 
+       ; return (Dict name pred inst_loc) }
 
 -- For vanilla implicit parameters, there is only one in scope
 -- at any time, so we used to use the name of the implicit parameter itself
 -- But with splittable implicit parameters there may be many in 
--- scope, so we make up a new name.
+-- scope, so we make up a new namea.
 newIPDict :: InstOrigin -> IPName Name -> Type 
          -> TcM (IPName Id, Inst)
 newIPDict orig ip_name ty
@@ -265,7 +276,7 @@ tcInstStupidTheta data_con inst_tys
        ; extendLIEs stupid_dicts }
   where
     stupid_theta = dataConStupidTheta data_con
-    tenv = zipTopTvSubst (dataConTyVars data_con) inst_tys
+    tenv = zipTopTvSubst (dataConUnivTyVars data_con) inst_tys
 
 newMethodFromName :: InstOrigin -> BoxyRhoType -> Name -> TcM TcId
 newMethodFromName origin ty name
@@ -580,8 +591,9 @@ lookupInst :: Inst -> TcM LookupInstResult
 -- Methods
 
 lookupInst inst@(Method _ id tys theta loc)
-  = newDictsAtLoc loc theta            `thenM` \ dicts ->
-    returnM (GenInst dicts (mkHsDictApp (mkHsTyApp (L span (HsVar id)) tys) (map instToId dicts)))
+  = do { dicts <- newDictsAtLoc loc theta
+       ; let co_fn = mkInstCoFn tys dicts
+       ; return (GenInst dicts (L span $ HsCoerce co_fn (HsVar id))) }
   where
     span = instLocSrcSpan loc
 
@@ -654,14 +666,15 @@ lookupInst (Dict _ pred loc)
                -- any nested for-alls in rho.  So the in-scope set is unchanged
        dfun_rho   = substTy tenv' rho
        (theta, _) = tcSplitPhiTy dfun_rho
-       ty_app     = mkHsTyApp (L (instLocSrcSpan loc) (HsVar dfun_id)) 
-                              (map (substTyVar tenv') tyvars)
+       src_loc    = instLocSrcSpan loc
+       dfun       = HsVar dfun_id
+       tys        = map (substTyVar tenv') tyvars
     ; if null theta then
-       returnM (SimpleInst ty_app)
+       returnM (SimpleInst (L src_loc $ HsCoerce (CoTyApps tys) dfun))
       else do
     { dicts <- newDictsAtLoc loc theta
-    ; let rhs = mkHsDictApp ty_app (map instToId dicts)
-    ; returnM (GenInst dicts rhs)
+    ; let co_fn = mkInstCoFn tys dicts
+    ; returnM (GenInst dicts (L src_loc $ HsCoerce co_fn dfun))
     }}}}
 
 ---------------
index 3bfa9b4..b4afcaf 100644 (file)
@@ -22,7 +22,8 @@ import TcType ( TcType, TcTauType, BoxyRhoType, mkFunTys, mkTyConApp,
 import TcMType ( newFlexiTyVarTy, tcInstSkolTyVars, zonkTcType )
 import TcBinds ( tcLocalBinds )
 import TcSimplify ( tcSimplifyCheck )
-import TcPat   ( tcPat, tcPats, PatCtxt(..) )
+import TcGadt  ( Refinement, emptyRefinement, refineResType )
+import TcPat   ( tcLamPat, tcLamPats )
 import TcUnify ( checkSigTyVarsWrt, boxySplitAppTy )
 import TcRnMonad
 import Inst    ( tcSyntaxName )
@@ -32,7 +33,7 @@ import VarSet
 import TysPrim ( alphaTyVar )
 import Type    ( Kind, mkArrowKinds, liftedTypeKind, openTypeKind, tyVarsOfTypes )
 
-import SrcLoc  ( Located(..) )
+import SrcLoc  ( Located(..), noLoc, unLoc )
 import Outputable
 import Util    ( lengthAtLeast )
 
@@ -54,8 +55,8 @@ tcProc pat cmd exp_ty
     do { (exp_ty1, res_ty) <- boxySplitAppTy exp_ty 
        ; (arr_ty, arg_ty)  <- boxySplitAppTy exp_ty1
        ; let cmd_env = CmdEnv { cmd_arr = arr_ty }
-       ; (pat', cmd') <- tcPat LamPat pat arg_ty res_ty $ \ res_ty' ->
-                         tcCmdTop cmd_env cmd ([], res_ty')
+       ; (pat', cmd') <- tcLamPat pat arg_ty (emptyRefinement, res_ty) $
+                         tcCmdTop cmd_env cmd []
        ; return (pat', cmd') }
 \end{code}
 
@@ -79,20 +80,29 @@ mkCmdArrTy env t1 t2 = mkAppTys (cmd_arr env) [t1, t2]
 ---------------------------------------
 tcCmdTop :: CmdEnv 
          -> LHsCmdTop Name
-         -> (CmdStack, TcTauType)      -- Expected result type; always a monotype
+         -> CmdStack
+        -> (Refinement, TcTauType)     -- Expected result type; always a monotype
                                        -- We know exactly how many cmd args are expected,
                                        -- albeit perhaps not their types; so we can pass 
                                        -- in a CmdStack
         -> TcM (LHsCmdTop TcId)
 
-tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) (cmd_stk, res_ty)
+tcCmdTop env (L loc (HsCmdTop cmd _ _ names)) cmd_stk reft_res_ty@(_,res_ty)
   = setSrcSpan loc $
-    do { cmd'   <- tcCmd env cmd (cmd_stk, res_ty)
+    do { cmd'   <- tcGuardedCmd env cmd cmd_stk reft_res_ty
        ; names' <- mapM (tcSyntaxName ProcOrigin (cmd_arr env)) names
        ; return (L loc $ HsCmdTop cmd' cmd_stk res_ty names') }
 
 
 ----------------------------------------
+tcGuardedCmd :: CmdEnv -> LHsExpr Name -> CmdStack
+            -> (Refinement, TcTauType) -> TcM (LHsExpr TcId)
+-- A wrapper that deals with the refinement (if any)
+tcGuardedCmd env expr stk (reft, res_ty)
+  = do { let (co, res_ty') = refineResType reft res_ty
+       ; body <- tcCmd env expr (stk, res_ty')
+       ; return (mkLHsCoerce co body) }
+
 tcCmd :: CmdEnv -> LHsExpr Name -> (CmdStack, TcTauType) -> TcM (LHsExpr TcId)
        -- The main recursive function
 tcCmd env (L loc expr) res_ty
@@ -120,7 +130,7 @@ tc_cmd env in_cmd@(HsCase scrut matches) (stk, res_ty)
   where
     match_ctxt = MC { mc_what = CaseAlt,
                       mc_body = mc_body }
-    mc_body body res_ty' = tcCmd env body (stk, res_ty')
+    mc_body body res_ty' = tcGuardedCmd env body stk res_ty'
 
 tc_cmd env (HsIf pred b1 b2) res_ty
   = do         { pred' <- tcMonoExpr pred boolTy
@@ -169,7 +179,6 @@ tc_cmd env cmd@(HsApp fun arg) (cmd_stk, res_ty)
 -------------------------------------------
 --             Lambda
 
--- gaw 2004
 tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig grhss))] _))
        (cmd_stk, res_ty)
   = addErrCtxt (matchCtxt match_ctxt match)    $
@@ -180,7 +189,7 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g
 
                -- Check the patterns, and the GRHSs inside
        ; (pats', grhss') <- setSrcSpan mtch_loc                $
-                            tcPats LamPat pats cmd_stk res_ty  $
+                            tcLamPats pats cmd_stk res_ty      $
                             tc_grhss grhss
 
        ; let match' = L mtch_loc (Match pats' Nothing grhss')
@@ -199,9 +208,8 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g
             ; return (GRHSs grhss' binds') }
 
     tc_grhs res_ty (GRHS guards body)
-       = do { (guards', rhs') <- tcStmts pg_ctxt tcGuardStmt
-                                         guards res_ty
-                                         (\res_ty' -> tcCmd env body (stk', res_ty'))
+       = do { (guards', rhs') <- tcStmts pg_ctxt tcGuardStmt guards res_ty $
+                                 tcGuardedCmd env body stk'
             ; return (GRHS guards' rhs') }
 
 -------------------------------------------
@@ -209,8 +217,8 @@ tc_cmd env cmd@(HsLam (MatchGroup [L mtch_loc (match@(Match pats maybe_rhs_sig g
 
 tc_cmd env cmd@(HsDo do_or_lc stmts body ty) (cmd_stk, res_ty)
   = do         { checkTc (null cmd_stk) (nonEmptyCmdStkErr cmd)
-       ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts res_ty $ \ res_ty' ->
-                            tcCmd env body ([], res_ty')
+       ; (stmts', body') <- tcStmts do_or_lc tc_stmt stmts (emptyRefinement, res_ty) $
+                            tcGuardedCmd env body []
        ; return (HsDo do_or_lc stmts' body' res_ty) }
   where
     tc_stmt = tcMDoStmt tc_rhs
@@ -256,7 +264,9 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
                -- the s1..sm and check each cmd
        ; cmds' <- mapM (tc_cmd w_tv) cmds_w_tys
 
-       ; returnM (HsArrForm (mkHsTyLam [w_tv] (mkHsDictLet inst_binds expr')) fixity cmds')
+       ; returnM (HsArrForm (noLoc $ HsCoerce (CoTyLams [w_tv]) 
+                                              (unLoc $ mkHsDictLet inst_binds expr')) 
+                            fixity cmds')
        }
   where
        -- Make the types       
@@ -264,7 +274,6 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
     new_cmd_ty :: LHsCmdTop Name -> Int
               -> TcM (LHsCmdTop Name, Int, TcType, TcType, TcType)
     new_cmd_ty cmd i
--- gaw 2004 FIX?
          = do  { b_ty   <- newFlexiTyVarTy arrowTyConKind
                ; tup_ty <- newFlexiTyVarTy liftedTypeKind
                        -- We actually make a type variable for the tuple
@@ -284,7 +293,7 @@ tc_cmd env cmd@(HsArrForm expr fixity cmd_args) (cmd_stk, res_ty)
                      not (w_tv `elemVarSet` tyVarsOfTypes arg_tys))
                     (badFormFun i tup_ty')
 
-          ; tcCmdTop (env { cmd_arr = b }) cmd (arg_tys, s) }
+          ; tcCmdTop (env { cmd_arr = b }) cmd arg_tys (emptyRefinement, s) }
 
     unscramble :: TcType -> (TcType, [TcType])
     -- unscramble ((w,s1) .. sn)       =  (w, [s1..sn])
index 7b4e5ec..9cc66e3 100644 (file)
@@ -30,14 +30,14 @@ import TcHsSyn              ( zonkId )
 import TcRnMonad
 import Inst            ( newDictsAtLoc, newIPDict, instToId )
 import TcEnv           ( tcExtendIdEnv, tcExtendIdEnv2, tcExtendTyVarEnv2, 
-                         pprBinders, tcLookupLocalId_maybe, tcLookupId,
+                         pprBinders, tcLookupId,
                          tcGetGlobalTyVars )
 import TcUnify         ( tcInfer, tcSubExp, unifyTheta, 
                          bleatEscapedTvs, sigCtxt )
 import TcSimplify      ( tcSimplifyInfer, tcSimplifyInferCheck, 
                          tcSimplifyRestricted, tcSimplifyIPs )
 import TcHsType                ( tcHsSigType, UserTypeCtxt(..) )
-import TcPat           ( tcPat, PatCtxt(..) )
+import TcPat           ( tcLetPat )
 import TcSimplify      ( bindInstsOfLocalFuns )
 import TcMType         ( newFlexiTyVarTy, zonkQuantifiedTyVar, zonkSigTyVar,
                          tcInstSigTyVars, tcInstSkolTyVars, tcInstType, 
@@ -48,9 +48,8 @@ import TcType         ( TcType, TcTyVar, TcThetaType,
                          mkTyVarTy, mkForAllTys, mkFunTys, exactTyVarsOfType, 
                          mkForAllTy, isUnLiftedType, tcGetTyVar, 
                          mkTyVarTys, tidyOpenTyVar )
-import Kind            ( argTypeKind )
+import {- Kind parts of -} Type                ( argTypeKind )
 import VarEnv          ( TyVarEnv, emptyVarEnv, lookupVarEnv, extendVarEnv ) 
-import TysWiredIn      ( unitTy )
 import TysPrim         ( alphaTyVar )
 import Id              ( Id, mkLocalId, mkVanillaGlobal )
 import IdInfo          ( vanillaIdInfo )
@@ -323,7 +322,7 @@ tcPolyBinds top_lvl sig_fn prag_fn rec_group rec_tc binds
     in
        -- SET UP THE MAIN RECOVERY; take advantage of any type sigs
     setSrcSpan loc                             $
-    recoverM (recoveryCode binder_names)       $ do 
+    recoverM (recoveryCode binder_names sig_fn)        $ do 
 
   { traceTc (ptext SLIT("------------------------------------------------"))
   ; traceTc (ptext SLIT("Bindings for") <+> ppr binder_names)
@@ -448,15 +447,14 @@ tcSpecPrag poly_id hs_ty inl
 -- If typechecking the binds fails, then return with each
 -- signature-less binder given type (forall a.a), to minimise 
 -- subsequent error messages
-recoveryCode binder_names
+recoveryCode binder_names sig_fn
   = do { traceTc (text "tcBindsWithSigs: error recovery" <+> ppr binder_names)
        ; poly_ids <- mapM mk_dummy binder_names
        ; return ([], poly_ids) }
   where
-    mk_dummy name = do { mb_id <- tcLookupLocalId_maybe name
-                       ; case mb_id of
-                             Just id -> return id              -- Had signature, was in envt
-                             Nothing -> return (mkLocalId name forall_a_a) }    -- No signature
+    mk_dummy name 
+       | isJust (sig_fn name) = tcLookupId name        -- Had signature; look it up
+       | otherwise            = return (mkLocalId name forall_a_a)    -- No signature
 
 forall_a_a :: TcType
 forall_a_a = mkForAllTy alphaTyVar (mkTyVarTy alphaTyVar)
@@ -651,9 +649,8 @@ tcLhs sig_fn bind@(PatBind { pat_lhs = pat, pat_rhs = grhss })
                                      | (name, Just sig) <- nm_sig_prs]
              sig_tau_fn  = lookupNameEnv tau_sig_env
 
-             tc_pat exp_ty = tcPat (LetPat sig_tau_fn) pat exp_ty unitTy $ \ _ ->
+             tc_pat exp_ty = tcLetPat sig_tau_fn pat exp_ty $
                              mapM lookup_info nm_sig_prs
-               -- The unitTy is a bit bogus; it's the "result type" for lookup_info.  
 
                -- After typechecking the pattern, look up the binder
                -- names, which the pattern has brought into scope.
index 0a8a498..46e702c 100644 (file)
@@ -39,14 +39,14 @@ import Maybes               ( catMaybes )
 import RdrName         ( RdrName )
 import Name            ( Name, getSrcLoc )
 import NameSet         ( duDefs )
-import Kind            ( splitKindFunTys )
+import Type            ( splitKindFunTys )
 import TyCon           ( tyConTyVars, tyConDataCons, tyConArity, tyConHasGenerics,
                          tyConStupidTheta, isProductTyCon, isDataTyCon, newTyConRhs,
                          isEnumerationTyCon, isRecursiveTyCon, TyCon
                        )
 import TcType          ( TcType, ThetaType, mkTyVarTys, mkTyConApp, tcTyConAppTyCon,
                          isUnLiftedType, mkClassPred, tyVarsOfType,
-                         isArgTypeKind, tcEqTypes, tcSplitAppTys, mkAppTys )
+                         isSubArgTypeKind, tcEqTypes, tcSplitAppTys, mkAppTys )
 import Var             ( TyVar, tyVarKind, varName )
 import VarSet          ( mkVarSet, subVarSet )
 import PrelNames
@@ -653,7 +653,7 @@ cond_typeableOK :: Condition
 --           (b) 7 or fewer args
 cond_typeableOK (gla_exts, tycon)
   | tyConArity tycon > 7                                     = Just too_many
-  | not (all (isArgTypeKind . tyVarKind) (tyConTyVars tycon)) = Just bad_kind
+  | not (all (isSubArgTypeKind . tyVarKind) (tyConTyVars tycon)) = Just bad_kind
   | otherwise                                                = Nothing
   where
     too_many = quotes (ppr tycon) <+> ptext SLIT("has too many arguments")
index be1ce9b..19deca9 100644 (file)
@@ -19,7 +19,7 @@ module TcEnv(
        tcExtendKindEnv, tcExtendKindEnvTvs,
        tcExtendTyVarEnv, tcExtendTyVarEnv2, 
        tcExtendIdEnv, tcExtendIdEnv1, tcExtendIdEnv2, 
-       tcLookup, tcLookupLocated, tcLookupLocalIds, tcLookupLocalId_maybe,
+       tcLookup, tcLookupLocated, tcLookupLocalIds, 
        tcLookupId, tcLookupTyVar, getScopedTyVarBinds,
        lclEnvElts, getInLocalScope, findGlobals, 
        wrongThingErr, pprBinders,
@@ -44,7 +44,8 @@ module TcEnv(
 #include "HsVersions.h"
 
 import HsSyn           ( LRuleDecl, LHsBinds, LSig, 
-                         LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds )
+                         LHsTyVarBndr, HsTyVarBndr(..), pprLHsBinds,
+                         ExprCoFn(..), idCoercion, (<.>) )
 import TcIface         ( tcImportDecl )
 import IfaceEnv                ( newGlobalBinder )
 import TcRnMonad
@@ -54,6 +55,7 @@ import TcType         ( Type, TcKind, TcTyVar, TcTyVarSet, TcType, TvSubst,
                          getDFunTyKey, tcTyConAppTyCon, tcGetTyVar, mkTyVarTy,
                          tidyOpenType, isRefineableTy
                        )
+import TcGadt          ( Refinement, refineType )
 import qualified Type  ( getTyVar_maybe )
 import Id              ( idName, isLocalId, setIdType )
 import Var             ( TyVar, Id, idType, tyVarName )
@@ -216,21 +218,16 @@ tcLookupTyVar name
        other       -> pprPanic "tcLookupTyVar" (ppr name)
 
 tcLookupId :: Name -> TcM Id
--- Used when we aren't interested in the binding level
--- Never a DataCon. (Why does that matter? see TcExpr.tcId)
+-- Used when we aren't interested in the binding level, nor refinement. 
+-- The "no refinement" part means that we return the un-refined Id regardless
+-- 
+-- The Id is never a DataCon. (Why does that matter? see TcExpr.tcId)
 tcLookupId name
   = tcLookup name      `thenM` \ thing -> 
     case thing of
-       ATcId tc_id _ _   -> returnM tc_id
-       AGlobal (AnId id) -> returnM id
-       other             -> pprPanic "tcLookupId" (ppr name)
-
-tcLookupLocalId_maybe :: Name -> TcM (Maybe Id)
-tcLookupLocalId_maybe name
-  = getLclEnv          `thenM` \ local_env ->
-    case lookupNameEnv (tcl_env local_env) name of
-       Just (ATcId tc_id _ _) -> return (Just tc_id)
-       other                  -> return Nothing
+       ATcId { tct_id = id} -> returnM id
+       AGlobal (AnId id)    -> returnM id
+       other                -> pprPanic "tcLookupId" (ppr name)
 
 tcLookupLocalIds :: [Name] -> TcM [TcId]
 -- We expect the variables to all be bound, and all at
@@ -241,8 +238,9 @@ tcLookupLocalIds ns
   where
     lookup lenv lvl name 
        = case lookupNameEnv lenv name of
-               Just (ATcId id lvl1 _) -> ASSERT( lvl == lvl1 ) id
-               other                  -> pprPanic "tcLookupLocalIds" (ppr name)
+               Just (ATcId { tct_id = id, tct_level = lvl1 }) 
+                       -> ASSERT( lvl == lvl1 ) id
+               other   -> pprPanic "tcLookupLocalIds" (ppr name)
 
 lclEnvElts :: TcLclEnv -> [TcTyThing]
 lclEnvElts env = nameEnvElts (tcl_env env)
@@ -322,8 +320,13 @@ tcExtendIdEnv2 names_w_ids thing_inside
     let
        extra_global_tyvars = tcTyVarsOfTypes [idType id | (_,id) <- names_w_ids]
        th_lvl              = thLevel (tcl_th_ctxt   env)
-       extra_env           = [ (name, ATcId id th_lvl (isRefineableTy (idType id)))
-                             | (name,id) <- names_w_ids]
+       extra_env           = [ (name, ATcId { tct_id = id, 
+                                              tct_level = th_lvl,
+                                              tct_type = id_ty, 
+                                              tct_co = if isRefineableTy id_ty 
+                                                       then Just idCoercion
+                                                       else Nothing })
+                             | (name,id) <- names_w_ids, let id_ty = idType id]
        le'                 = extendNameEnvList (tcl_env env) extra_env
        rdr_env'            = extendLocalRdrEnv (tcl_rdr env) [name | (name,_) <- names_w_ids]
     in
@@ -360,7 +363,7 @@ findGlobals tvs tidy_env
     ignore_it ty = not (tvs `intersectsVarSet` tyVarsOfType ty)
 
 -----------------------
-find_thing ignore_it tidy_env (ATcId id _ _)
+find_thing ignore_it tidy_env (ATcId { tct_id = id })
   = zonkTcType  (idType id)    `thenM` \ id_ty ->
     if ignore_it id_ty then
        returnM (tidy_env, Nothing)
@@ -393,16 +396,20 @@ find_thing _ _ thing = pprPanic "find_thing" (ppr thing)
 \end{code}
 
 \begin{code}
-refineEnvironment :: TvSubst -> TcM a -> TcM a
+refineEnvironment :: Refinement -> TcM a -> TcM a
+-- I don't think I have to refine the set of global type variables in scope
+-- Reason: the refinement never increases that set
 refineEnvironment reft thing_inside
   = do { env <- getLclEnv
        ; let le' = mapNameEnv refine (tcl_env env)
-       ; gtvs' <- refineGlobalTyVars reft (tcl_tyvars env) 
-       ; setLclEnv (env {tcl_env = le', tcl_tyvars = gtvs'}) thing_inside }
+       ; setLclEnv (env {tcl_env = le'}) thing_inside }
   where
-    refine (ATcId id lvl True) = ATcId (setIdType id (substTy reft (idType id))) lvl True
-    refine (ATyVar tv ty)      = ATyVar tv (substTy reft ty)
-    refine elt                = elt
+    refine elt@(ATcId { tct_co = Just co, tct_type = ty })
+                         = let (co', ty') = refineType reft ty
+                           in elt { tct_co = Just (co' <.> co), tct_type = ty' }
+    refine (ATyVar tv ty) = ATyVar tv (snd (refineType reft ty))
+                               -- Ignore the coercion that refineType returns
+    refine elt           = elt
 \end{code}
 
 %************************************************************************
@@ -415,11 +422,6 @@ refineEnvironment reft thing_inside
 tc_extend_gtvs gtvs extra_global_tvs
   = readMutVar gtvs            `thenM` \ global_tvs ->
     newMutVar (global_tvs `unionVarSet` extra_global_tvs)
-
-refineGlobalTyVars :: GadtRefinement -> TcRef TcTyVarSet -> TcM (TcRef TcTyVarSet)
-refineGlobalTyVars reft gtv_var
-  = readMutVar gtv_var                         `thenM` \ gbl_tvs ->
-    newMutVar (tcTyVarsOfTypes (map (substTyVar reft) (varSetElems gbl_tvs)))
 \end{code}
 
 @tcGetGlobalTyVars@ returns a fully-zonked set of tyvars free in the environment.
index 0da370b..43360c7 100644 (file)
@@ -21,39 +21,47 @@ import qualified DsMeta
 #endif
 
 import HsSyn           ( HsExpr(..), LHsExpr, ArithSeqInfo(..), recBindFields,
-                         HsMatchContext(..), HsRecordBinds, 
-                         mkHsCoerce, mkHsApp, mkHsDictApp, mkHsTyApp )
+                         HsMatchContext(..), HsRecordBinds, mkHsCoerce,
+                         mkHsApp )
 import TcHsSyn         ( hsLitType )
 import TcRnMonad
 import TcUnify         ( tcInfer, tcSubExp, tcFunResTy, tcGen, boxyUnify, subFunTys, zapToMonotype, stripBoxyType,
                          boxySplitListTy, boxySplitTyConApp, wrapFunResCoercion, preSubType,
                          unBox )
 import BasicTypes      ( Arity, isMarkedStrict )
-import Inst            ( newMethodFromName, newIPDict, instToId,
+import Inst            ( newMethodFromName, newIPDict, mkInstCoFn,
                          newDicts, newMethodWithGivenTy, tcInstStupidTheta )
 import TcBinds         ( tcLocalBinds )
-import TcEnv           ( tcLookup, tcLookupId, tcLookupDataCon, tcLookupField )
+import TcEnv           ( tcLookup, tcLookupDataCon, tcLookupField )
 import TcArrows                ( tcProc )
-import TcMatches       ( tcMatchesCase, tcMatchLambda, tcDoStmts, TcMatchCtxt(..) )
+import TcMatches       ( tcMatchesCase, tcMatchLambda, tcDoStmts, tcBody,
+                         TcMatchCtxt(..) )
 import TcHsType                ( tcHsSigType, UserTypeCtxt(..) )
 import TcPat           ( tcOverloadedLit, badFieldCon )
-import TcMType         ( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars, readFilledBox, zonkTcTypes )
-import TcType          ( TcType, TcSigmaType, TcRhoType, 
+import TcMType         ( tcInstTyVars, newFlexiTyVarTy, newBoxyTyVars,
+                         readFilledBox, zonkTcTypes )
+import TcType          ( TcType, TcSigmaType, TcRhoType, TvSubst,
                          BoxySigmaType, BoxyRhoType, ThetaType,
                          mkTyVarTys, mkFunTys, 
-                         tcMultiSplitSigmaTy, tcSplitFunTysN, tcSplitTyConApp_maybe,
+                         tcMultiSplitSigmaTy, tcSplitFunTysN,
+                         tcSplitTyConApp_maybe, 
                          isSigmaTy, mkFunTy, mkTyConApp, isLinearPred,
                          exactTyVarsOfType, exactTyVarsOfTypes, 
                          zipTopTvSubst, zipOpenTvSubst, substTys, substTyVar
                        )
-import Kind            ( argTypeKind )
-
-import Id              ( Id, idType, idName, recordSelectorFieldLabel, 
-                         isRecordSelector, isNaughtyRecordSelector, isDataConId_maybe )
-import DataCon         ( DataCon, dataConFieldLabels, dataConStrictMarks, dataConSourceArity,
-                         dataConWrapId, isVanillaDataCon, dataConTyVars, dataConOrigArgTys )
+import {- Kind parts of -} 
+       Type            ( argTypeKind )
+
+import Id              ( Id, idType, recordSelectorFieldLabel,
+                         isRecordSelector, isNaughtyRecordSelector,
+                         isDataConId_maybe )
+import DataCon         ( DataCon, dataConFieldLabels, dataConStrictMarks,
+                         dataConSourceArity, 
+                         dataConWrapId, isVanillaDataCon, dataConUnivTyVars,
+                         dataConOrigArgTys ) 
 import Name            ( Name )
-import TyCon           ( FieldLabel, tyConStupidTheta, tyConDataCons, isEnumerationTyCon )
+import TyCon           ( FieldLabel, tyConStupidTheta, tyConDataCons,
+                         isEnumerationTyCon ) 
 import Type            ( substTheta, substTy )
 import Var             ( TyVar, tyVarKind )
 import VarSet          ( emptyVarSet, elemVarSet, unionVarSet )
@@ -68,7 +76,7 @@ import PrimOp         ( tagToEnumKey )
 import DynFlags
 import StaticFlags     ( opt_NoMethodSharing )
 import HscTypes                ( TyThing(..) )
-import SrcLoc          ( Located(..), unLoc, noLoc, getLoc )
+import SrcLoc          ( Located(..), unLoc, getLoc )
 import Util
 import ListSetOps      ( assocMaybe )
 import Maybes          ( catMaybes )
@@ -282,7 +290,7 @@ tcExpr (HsCase scrut matches) exp_ty
        ; return (HsCase scrut' matches') }
  where
     match_ctxt = MC { mc_what = CaseAlt,
-                     mc_body = tcPolyExpr }
+                     mc_body = tcBody }
 
 tcExpr (HsIf pred b1 b2) res_ty
   = do { pred' <- addErrCtxt (predCtxt pred) $
@@ -440,7 +448,7 @@ tcExpr expr@(RecordUpd record_expr rbinds _ _) res_ty
                -- A constructor is only relevant to this process if
                -- it contains *all* the fields that are being updated
        con1            = head relevant_cons    -- A representative constructor
-       con1_tyvars     = dataConTyVars con1
+       con1_tyvars     = dataConUnivTyVars con1 
        con1_flds       = dataConFieldLabels con1
        con1_arg_tys    = dataConOrigArgTys con1
        common_tyvars   = exactTyVarsOfTypes [ty | (fld,ty) <- con1_flds `zip` con1_arg_tys
@@ -633,10 +641,11 @@ tcIdApp :: Name                                   -- Function
 -- Then                fres <= bx_(k+1) -> ... -> bx_n -> res_ty
 
 tcIdApp fun_name n_args arg_checker res_ty
-  = do { fun_id <- lookupFun (OccurrenceOf fun_name) fun_name
+  = do { let orig = OccurrenceOf fun_name
+       ; (fun, fun_ty) <- lookupFun orig fun_name
 
        -- Split up the function type
-       ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy (idType fun_id)
+       ; let (tv_theta_prs, rho) = tcMultiSplitSigmaTy fun_ty
              (fun_arg_tys, fun_res_ty) = tcSplitFunTysN rho n_args
 
              qtvs = concatMap fst tv_theta_prs         -- Quantified tyvars
@@ -678,7 +687,7 @@ tcIdApp fun_name n_args arg_checker res_ty
        -- And pack up the results
        -- By applying the coercion just to the *function* we can make
        -- tcFun work nicely for OpApp and Sections too
-       ; fun' <- instFun fun_id qtvs qtys'' tv_theta_prs
+       ; fun' <- instFun orig fun res_subst tv_theta_prs
        ; co_fn' <- wrapFunResCoercion fun_arg_tys' co_fn
        ; return (mkHsCoerce co_fn' fun', args') }
 \end{code}
@@ -707,10 +716,10 @@ tcId :: InstOrigin
      -> TcM (HsExpr TcId)
 tcId orig fun_name res_ty
   = do { traceTc (text "tcId" <+> ppr fun_name <+> ppr res_ty)
-       ; fun_id <- lookupFun orig fun_name
+       ; (fun, fun_ty) <- lookupFun orig fun_name
 
        -- Split up the function type
-       ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy (idType fun_id)
+       ; let (tv_theta_prs, fun_tau) = tcMultiSplitSigmaTy fun_ty
              qtvs = concatMap fst tv_theta_prs -- Quantified tyvars
              tau_qtvs = exactTyVarsOfType fun_tau      -- Mentioned in the tau part
        ; qtv_tys <- preSubType qtvs tau_qtvs fun_tau res_ty
@@ -722,7 +731,7 @@ tcId orig fun_name res_ty
        ; co_fn <- tcFunResTy fun_name fun_tau' res_ty
 
        -- And pack up the results
-       ; fun' <- instFun fun_id qtvs qtv_tys tv_theta_prs 
+       ; fun' <- instFun orig fun res_subst tv_theta_prs 
        ; return (mkHsCoerce co_fn fun') }
 
 --     Note [Push result type in]
@@ -756,49 +765,49 @@ tcSyntaxOp orig (HsVar op) ty = tcId orig op ty
 tcSyntaxOp orig other     ty = pprPanic "tcSyntaxOp" (ppr other)
 
 ---------------------------
-instFun :: TcId
-       -> [TyVar] -> [TcType]  -- Quantified type variables and 
-                               -- their instantiating types
-       -> [([TyVar], ThetaType)]       -- Stuff to instantiate
+instFun :: InstOrigin
+       -> HsExpr TcId
+       -> TvSubst                -- The instantiating substitution
+       -> [([TyVar], ThetaType)] -- Stuff to instantiate
        -> TcM (HsExpr TcId)    
-instFun fun_id qtvs qtv_tys []
-  = return (HsVar fun_id)      -- Common short cut
 
-instFun fun_id qtvs qtv_tys tv_theta_prs
-  = do         {       -- Horrid check for tagToEnum; see Note [tagToEnum#]
-         checkBadTagToEnumCall fun_id qtv_tys
+instFun orig fun subst []
+  = return fun         -- Common short cut
 
-       ; let subst = zipOpenTvSubst qtvs qtv_tys
-             ty_theta_prs' = map subst_pr tv_theta_prs
-             subst_pr (tvs, theta) = (map (substTyVar subst) tvs, 
-                                      substTheta subst theta)
+instFun orig fun subst tv_theta_prs
+  = do         {-- !!!SPJ:     -- Horrid check for tagToEnum; see Note [tagToEnum#]
+        -- !!!SPJ: checkBadTagToEnumCall fun_id qtv_tys
+
+       ; let ty_theta_prs' = map subst_pr tv_theta_prs
 
-               -- The ty_theta_prs' is always non-empty
-             ((tys1',theta1') : further_prs') = ty_theta_prs'
-               
                -- First, chuck in the constraints from 
                -- the "stupid theta" of a data constructor (sigh)
-       ; case isDataConId_maybe fun_id of
-               Just con -> tcInstStupidTheta con tys1'
-               Nothing  -> return ()
-
-       ; if want_method_inst theta1'
-         then do { meth_id <- newMethodWithGivenTy orig fun_id tys1'
-                       -- See Note [Multiple instantiation]
-                 ; go (HsVar meth_id) further_prs' }
-         else go (HsVar fun_id) ty_theta_prs'
-       }
+       ; inst_stupid fun ty_theta_prs'
+
+               -- Now do normal instantiation
+       ; go True fun ty_theta_prs' }
   where
-    orig = OccurrenceOf (idName fun_id)
+    subst_pr (tvs, theta) 
+       = (map (substTyVar subst) tvs, substTheta subst theta)
+
+    inst_stupid (HsVar fun_id) ((tys,_):_)
+       | Just con <- isDataConId_maybe fun_id = tcInstStupidTheta con tys
+    inst_stupid _ _ = return ()
+
+    go _ fun [] = return fun
 
-    go fun [] = return fun
+    go True (HsVar fun_id) ((tys,theta) : prs)
+       | want_method_inst theta
+       = do { meth_id <- newMethodWithGivenTy orig fun_id tys
+            ; go False (HsVar meth_id) prs }
+               -- Go round with 'False' to prevent further use
+               -- of newMethod: see Note [Multiple instantiation]
 
-    go fun ((tys, theta) : prs)
+    go fun ((tys, theta) : prs)
        = do { dicts <- newDicts orig theta
             ; extendLIEs dicts
-            ; let the_app = unLoc $ mkHsDictApp (mkHsTyApp (noLoc fun) tys)
-                                                (map instToId dicts)
-            ; go the_app prs }
+            ; let co_fn = mkInstCoFn tys dicts
+            ; go False (HsCoerce co_fn fun) prs }
 
        --      Hack Alert (want_method_inst)!
        -- See Note [No method sharing]
@@ -925,40 +934,53 @@ tagToEnumError tys
 %************************************************************************
 
 \begin{code}
-lookupFun :: InstOrigin -> Name -> TcM TcId
+lookupFun :: InstOrigin -> Name -> TcM (HsExpr TcId, TcType)
 lookupFun orig id_name
   = do         { thing <- tcLookup id_name
        ; case thing of
-           AGlobal (ADataCon con) -> return (dataConWrapId con)
+           AGlobal (ADataCon con) -> return (HsVar wrap_id, idType wrap_id)
+                                  where
+                                     wrap_id = dataConWrapId con
 
            AGlobal (AnId id) 
                | isNaughtyRecordSelector id -> failWithTc (naughtyRecordSel id)
-               | otherwise                  -> return id
+               | otherwise                  -> return (HsVar id, idType id)
                -- A global cannot possibly be ill-staged
                -- nor does it need the 'lifting' treatment
 
-#ifndef GHCI
-           ATcId id th_level _ -> return id                    -- Non-TH case
-#else
-           ATcId id th_level _ -> do { use_stage <- getStage   -- TH case
-                                     ; thLocalId orig id_name id th_level use_stage }
-#endif
+           ATcId { tct_id = id, tct_type = ty, tct_co = mb_co, tct_level = lvl }
+               -> do { thLocalId orig id ty lvl
+                     ; case mb_co of
+                         Nothing -> return (HsVar id, ty)      -- Wobbly, or no free vars
+                         Just co -> return (mkHsCoerce co (HsVar id), ty) }    
 
            other -> failWithTc (ppr other <+> ptext SLIT("used where a value identifer was expected"))
     }
 
-#ifdef GHCI  /* GHCI and TH is on */
+#ifndef GHCI  /* GHCI and TH is off */
 --------------------------------------
 -- thLocalId : Check for cross-stage lifting
+thLocalId orig id id_ty th_bind_lvl
+  = return ()
+
+#else        /* GHCI and TH is on */
+thLocalId orig id id_ty th_bind_lvl 
+  = do { use_stage <- getStage -- TH case
+       ; case use_stage of
+           Brack use_lvl ps_var lie_var | use_lvl > th_bind_lvl
+                 -> thBrackId orig id ps_var lie_var
+           other -> checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
+       }
+
 thLocalId orig id_name id th_bind_lvl (Brack use_lvl ps_var lie_var)
   | use_lvl > th_bind_lvl
-  = thBrackId orig id_name id ps_var lie_var
+  = thBrackId 
 thLocalId orig id_name id th_bind_lvl use_stage
-  = do { checkWellStaged (quotes (ppr id)) th_bind_lvl use_stage
+  = do { checkWellStaged 
        ; return id }
 
 --------------------------------------
-thBrackId orig id_name id ps_var lie_var
+thBrackId orig id ps_var lie_var
   | isExternalName id_name
   =    -- Top-level identifiers in this module,
        -- (which have External Names)
@@ -1005,6 +1027,8 @@ thBrackId orig id_name id ps_var lie_var
        ; writeMutVar ps_var ((id_name, nlHsApp (nlHsVar lift) (nlHsVar id)) : ps)
 
        ; return id } }
+ where
+   id_name = idName id
 #endif /* GHCI */
 \end{code}
 
@@ -1048,7 +1072,7 @@ tcRecordBinds data_con arg_tys rbinds
       | Just field_ty <- assocMaybe flds_w_tys field_lbl
       = addErrCtxt (fieldCtxt field_lbl)       $
        do { rhs'   <- tcPolyExprNC rhs field_ty
-          ; sel_id <- tcLookupId field_lbl
+          ; sel_id <- tcLookupField field_lbl
           ; ASSERT( isRecordSelector sel_id )
             return (Just (L loc sel_id, rhs')) }
       | otherwise
index bfec766..8ab91ce 100644 (file)
@@ -8,9 +8,9 @@ checker.
 
 \begin{code}
 module TcHsSyn (
-       mkHsTyApp, mkHsDictApp, mkHsConApp,
-       mkHsTyLam, mkHsDictLam, mkHsDictLet, mkHsApp,
-       hsLitType, hsPatType, mkHsAppTy, mkSimpleHsAlt,
+       mkHsConApp, mkHsDictLet, mkHsApp,
+       hsLitType, hsLPatType, hsPatType, 
+       mkHsAppTy, mkSimpleHsAlt,
        nlHsIntLit, mkVanillaTuplePat,
        
 
@@ -30,9 +30,8 @@ import HsSyn  -- oodles of it
 import Id      ( idType, setIdType, Id )
 
 import TcRnMonad
-import Type      ( Type )
+import Type      ( Type, isLiftedTypeKind, liftedTypeKind, isSubKind, eqKind  )
 import TcType    ( TcType, TcTyVar, mkTyVarTy, mkTyConApp, isImmutableTyVar )
-import Kind      ( isLiftedTypeKind, liftedTypeKind, isSubKind )
 import qualified  Type
 import TcMType   ( zonkQuantifiedTyVar, zonkType, zonkTcType, writeMetaTyVar )
 import TysPrim   ( charPrimTy, intPrimTy, floatPrimTy,
@@ -42,7 +41,7 @@ import TysWiredIn ( charTy, stringTy, intTy,
                    mkListTy, mkPArrTy, mkTupleTy, unitTy,
                    voidTy, listTyCon, tupleTyCon )
 import TyCon     ( mkPrimTyCon, tyConKind, PrimRep(..) )
-import Kind      ( splitKindFunTys )
+import {- Kind parts of -} Type          ( splitKindFunTys )
 import Name      ( Name, getOccName, mkInternalName, mkDerivedTyConOcc )
 import Var       ( Var, isId, isLocalVar, tyVarKind )
 import VarSet
@@ -63,33 +62,34 @@ import Outputable
 %*                                                                     *
 %************************************************************************
 
-Note: If @hsPatType@ doesn't bear a strong resemblance to @exprType@,
+Note: If @hsLPatType@ doesn't bear a strong resemblance to @exprType@,
 then something is wrong.
 \begin{code}
 mkVanillaTuplePat :: [OutPat Id] -> Boxity -> Pat Id
 -- A vanilla tuple pattern simply gets its type from its sub-patterns
 mkVanillaTuplePat pats box 
-  = TuplePat pats box (mkTupleTy box (length pats) (map hsPatType pats))
-
-hsPatType :: OutPat Id -> Type
-hsPatType (L _ pat) = pat_type pat
-
-pat_type (ParPat pat)             = hsPatType pat
-pat_type (WildPat ty)             = ty
-pat_type (VarPat var)             = idType var
-pat_type (VarPatOut var _)        = idType var
-pat_type (BangPat pat)            = hsPatType pat
-pat_type (LazyPat pat)            = hsPatType pat
-pat_type (LitPat lit)             = hsLitType lit
-pat_type (AsPat var pat)          = idType (unLoc var)
-pat_type (ListPat _ ty)                   = mkListTy ty
-pat_type (PArrPat _ ty)                   = mkPArrTy ty
-pat_type (TuplePat pats box ty)           = ty
-pat_type (ConPatOut _ _ _ _ _ ty)  = ty
-pat_type (SigPatOut pat ty)       = ty
-pat_type (NPat lit _ _ ty)        = ty
-pat_type (NPlusKPat id _ _ _)      = idType (unLoc id)
-pat_type (DictPat ds ms)           = case (ds ++ ms) of
+  = TuplePat pats box (mkTupleTy box (length pats) (map hsLPatType pats))
+
+hsLPatType :: OutPat Id -> Type
+hsLPatType (L _ pat) = hsPatType pat
+
+hsPatType (ParPat pat)             = hsLPatType pat
+hsPatType (WildPat ty)             = ty
+hsPatType (VarPat var)             = idType var
+hsPatType (VarPatOut var _)        = idType var
+hsPatType (BangPat pat)                    = hsLPatType pat
+hsPatType (LazyPat pat)                    = hsLPatType pat
+hsPatType (LitPat lit)             = hsLitType lit
+hsPatType (AsPat var pat)          = idType (unLoc var)
+hsPatType (ListPat _ ty)           = mkListTy ty
+hsPatType (PArrPat _ ty)           = mkPArrTy ty
+hsPatType (TuplePat pats box ty)    = ty
+hsPatType (ConPatOut{ pat_ty = ty })= ty
+hsPatType (SigPatOut pat ty)       = ty
+hsPatType (NPat lit _ _ ty)        = ty
+hsPatType (NPlusKPat id _ _ _)      = idType (unLoc id)
+hsPatType (CoPat _ _ ty)           = ty
+hsPatType (DictPat ds ms)           = case (ds ++ ms) of
                                       []  -> unitTy
                                       [d] -> idType d
                                       ds  -> mkTupleTy Boxed (length ds) (map idType ds)
@@ -495,28 +495,6 @@ zonkExpr env (HsCoreAnn lbl expr)
   = zonkLExpr env expr   `thenM` \ new_expr ->
     returnM (HsCoreAnn lbl new_expr)
 
-zonkExpr env (TyLam tyvars expr)
-  = ASSERT( all isImmutableTyVar tyvars )
-    zonkLExpr env expr                 `thenM` \ new_expr ->
-    returnM (TyLam tyvars new_expr)
-
-zonkExpr env (TyApp expr tys)
-  = zonkLExpr env expr         `thenM` \ new_expr ->
-    zonkTcTypeToTypes env tys  `thenM` \ new_tys ->
-    returnM (TyApp new_expr new_tys)
-
-zonkExpr env (DictLam dicts expr)
-  = zonkIdBndrs env dicts      `thenM` \ new_dicts ->
-    let
-       env1 = extendZonkEnv env new_dicts
-    in
-    zonkLExpr env1 expr        `thenM` \ new_expr ->
-    returnM (DictLam new_dicts new_expr)
-
-zonkExpr env (DictApp expr dicts)
-  = zonkLExpr env expr                 `thenM` \ new_expr ->
-    returnM (DictApp new_expr (zonkIdOccs env dicts))
-
 -- arrow notation extensions
 zonkExpr env (HsProc pat body)
   = do { (env1, new_pat) <- zonkPat env pat
@@ -554,24 +532,21 @@ zonk_cmd_top env (HsCmdTop cmd stack_tys ty ids)
 -------------------------------------------------------------------------
 zonkCoFn :: ZonkEnv -> ExprCoFn -> TcM (ZonkEnv, ExprCoFn)
 zonkCoFn env CoHole = return (env, CoHole)
+zonkCoFn env (ExprCoFn co)     = do { co' <- zonkTcTypeToType env co
+                                   ; return (env, ExprCoFn co') }
 zonkCoFn env (CoCompose c1 c2) = do { (env1, c1') <- zonkCoFn env c1
                                    ; (env2, c2') <- zonkCoFn env1 c2
                                    ; return (env2, CoCompose c1' c2') }
-zonkCoFn env (CoLams ids c) = do { ids' <- zonkIdBndrs env ids
+zonkCoFn env (CoLams ids)   = do { ids' <- zonkIdBndrs env ids
                                 ; let env1 = extendZonkEnv env ids'
-                                ; (env2, c') <- zonkCoFn env1 c
-                                ; return (env2, CoLams ids' c') }
-zonkCoFn env (CoTyLams tvs c) = ASSERT( all isImmutableTyVar tvs )
-                               do { (env1, c') <- zonkCoFn env c
-                                  ; return (env1, CoTyLams tvs c') }
-zonkCoFn env (CoApps c ids)   = do { (env1, c') <- zonkCoFn env c
-                                  ; return (env1, CoApps c' (zonkIdOccs env ids)) }
-zonkCoFn env (CoTyApps c tys) = do { tys' <- zonkTcTypeToTypes env tys
-                                  ; (env1, c') <- zonkCoFn env c
-                                  ; return (env1, CoTyApps c' tys') }
-zonkCoFn env (CoLet bs c)     = do { (env1, bs') <- zonkRecMonoBinds env bs
-                                  ; (env2, c')  <- zonkCoFn env1 c
-                                  ; return (env2, CoLet bs' c') }
+                                ; return (env1, CoLams ids') }
+zonkCoFn env (CoTyLams tvs) = ASSERT( all isImmutableTyVar tvs )
+                             do { return (env, CoTyLams tvs) }
+zonkCoFn env (CoApps ids)   = do { return (env, CoApps (zonkIdOccs env ids)) }
+zonkCoFn env (CoTyApps tys) = do { tys' <- zonkTcTypeToTypes env tys
+                                ; return (env, CoTyApps tys') }
+zonkCoFn env (CoLet bs)     = do { (env1, bs') <- zonkRecMonoBinds env bs
+                                ; return (env1, CoLet bs') }
 
 
 -------------------------------------------------------------------------
@@ -739,14 +714,15 @@ zonk_pat env (TuplePat pats boxed ty)
        ; (env', pats') <- zonkPats env pats
        ; return (env', TuplePat pats' boxed ty') }
 
-zonk_pat env (ConPatOut n tvs dicts binds stuff ty)
-  = ASSERT( all isImmutableTyVar tvs )
+zonk_pat env p@(ConPatOut { pat_ty = ty, pat_dicts = dicts, pat_binds = binds, pat_args = args })
+  = ASSERT( all isImmutableTyVar (pat_tvs p) ) 
     do { new_ty <- zonkTcTypeToType env ty
        ; new_dicts <- zonkIdBndrs env dicts
        ; let env1 = extendZonkEnv env new_dicts
        ; (env2, new_binds) <- zonkRecMonoBinds env1 binds
-       ; (env', new_stuff) <- zonkConStuff env2 stuff
-       ; returnM (env', ConPatOut n tvs new_dicts new_binds new_stuff new_ty) }
+       ; (env', new_args) <- zonkConStuff env2 args
+       ; returnM (env', p { pat_ty = new_ty, pat_dicts = new_dicts, 
+                            pat_binds = new_binds, pat_args = new_args }) }
 
 zonk_pat env (LitPat lit) = return (env, LitPat lit)
 
@@ -953,7 +929,7 @@ mkArbitraryType tv
     kind       = tyVarKind tv
     (args,res) = splitKindFunTys kind
 
-    tycon | kind == tyConKind listTyCon        --  *->*
+    tycon | eqKind kind (tyConKind listTyCon)  --  *->*
          = listTyCon                           -- No tuples this size
 
          | all isLiftedTypeKind args && isLiftedTypeKind res
index 8411631..6a43e23 100644 (file)
@@ -45,7 +45,7 @@ import TcType         ( Type, PredType(..), ThetaType, BoxySigmaType,
                          substTyWith, mkTyVarTys, tcEqType,
                          tcIsTyVarTy, mkFunTy, mkSigmaTy, mkPredTy, 
                          mkTyConApp, mkAppTys, typeKind )
-import Kind            ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
+import {- Kind parts of -} Type                ( Kind, isLiftedTypeKind, liftedTypeKind, ubxTupleKind, 
                          openTypeKind, argTypeKind, splitKindFunTys )
 import Var             ( TyVar, mkTyVar, tyVarName )
 import TyCon           ( TyCon, tyConKind )
index 11ec9d9..4542a34 100644 (file)
@@ -23,6 +23,10 @@ module TcMType (
   newBoxyTyVar, newBoxyTyVars, newBoxyTyVarTys, readFilledBox, 
 
   --------------------------------
+  -- Creating new coercion variables
+  newCoVars,
+
+  --------------------------------
   -- Instantiation
   tcInstTyVar, tcInstType, tcInstTyVars, tcInstBoxyTyVar,
   tcInstSigTyVars, zonkSigTyVar,
@@ -58,10 +62,11 @@ import TypeRep              ( Type(..), PredType(..),  -- Friend; can see representation
 import TcType          ( TcType, TcThetaType, TcTauType, TcPredType,
                          TcTyVarSet, TcKind, TcTyVar, TcTyVarDetails(..), 
                          MetaDetails(..), SkolemInfo(..), BoxInfo(..), 
-                         BoxyTyVar, BoxyType, UserTypeCtxt(..),
-                         isMetaTyVar, isSigTyVar, metaTvRef,
+                         BoxyTyVar, BoxyType, UserTypeCtxt(..), kindVarRef,
+                         mkKindVar, isMetaTyVar, isSigTyVar, metaTvRef,
                          tcCmpPred, isClassPred, tcGetTyVar,
-                         tcSplitPhiTy, tcSplitPredTy_maybe, tcSplitAppTy_maybe, 
+                         tcSplitPhiTy, tcSplitPredTy_maybe,
+                         tcSplitAppTy_maybe,  
                          tcValidInstHeadTy, tcSplitForAllTys,
                          tcIsTyVarTy, tcSplitSigmaTy, 
                          isUnLiftedType, isIPPred, 
@@ -70,21 +75,23 @@ import TcType               ( TcType, TcThetaType, TcTauType, TcPredType,
                          tyVarsOfPred, getClassPredTys_maybe,
                          tyVarsOfType, tyVarsOfTypes, tcView,
                          pprPred, pprTheta, pprClassPred )
-import Kind            ( Kind(..), KindVar, kindVarRef, mkKindVar, 
-                         isLiftedTypeKind, isArgTypeKind, isOpenTypeKind,
+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 )
+                         mkTyVar, mkTcTyVar, tcTyVarDetails,
+                         CoVar, mkCoVar )
 
        -- Assertions
 #ifdef DEBUG
 import TcType          ( isFlexi, isBoxyTyVar, isImmutableTyVar )
-import Kind            ( isSubKind )
+import Type            ( isSubKind )
 #endif
 
 -- others:
@@ -95,6 +102,7 @@ import VarSet
 import DynFlags                ( dopt, DynFlag(..) )
 import Util            ( nOfThem, isSingleton, notNull )
 import ListSetOps      ( removeDups )
+import UniqSupply      ( uniqsFromSupply )
 import Outputable
 
 import Control.Monad   ( when )
@@ -139,10 +147,17 @@ tcInstType inst_tyvars ty
 %************************************************************************
 
 \begin{code}
+newCoVars :: [(TcType,TcType)] -> TcM [CoVar]
+newCoVars spec
+  = do { us <- newUniqueSupply 
+       ; return [ mkCoVar (mkSysTvName uniq FSLIT("co"))
+                          (mkCoKind ty1 ty2)
+                | ((ty1,ty2), uniq) <- spec `zip` uniqsFromSupply us] }
+
 newKindVar :: TcM TcKind
 newKindVar = do        { uniq <- newUnique
-               ; ref <- newMutVar Nothing
-               ; return (KindVar (mkKindVar uniq ref)) }
+               ; ref <- newMutVar Flexi
+               ; return (mkTyVarTy (mkKindVar uniq ref)) }
 
 newKindVars :: Int -> TcM [TcKind]
 newKindVars n = mappM (\ _ -> newKindVar) (nOfThem n ())
@@ -442,6 +457,10 @@ zonkTcPredType (ClassP c ts)
 zonkTcPredType (IParam n t)
   = zonkTcType t       `thenM` \ new_t ->
     returnM (IParam n new_t)
+zonkTcPredType (EqPred t1 t2)
+  = zonkTcType t1      `thenM` \ new_t1 ->
+    zonkTcType t2      `thenM` \ new_t2 ->
+    returnM (EqPred new_t1 new_t2)
 \end{code}
 
 -------------------  These ...ToType, ...ToKind versions
@@ -566,10 +585,13 @@ zonkType unbound_var_fn ty
                             go ty              `thenM` \ ty' ->
                             returnM (ForAllTy tyvar ty')
 
-    go_pred (ClassP c tys) = mappM go tys      `thenM` \ tys' ->
-                            returnM (ClassP c tys')
-    go_pred (IParam n ty)  = go ty             `thenM` \ ty' ->
-                            returnM (IParam n ty')
+    go_pred (ClassP c tys)   = mappM go tys    `thenM` \ tys' ->
+                              returnM (ClassP c tys')
+    go_pred (IParam n ty)    = go ty           `thenM` \ ty' ->
+                              returnM (IParam n ty')
+    go_pred (EqPred ty1 ty2) = go ty1          `thenM` \ ty1' ->
+                              go ty2           `thenM` \ ty2' ->
+                              returnM (EqPred ty1' ty2')
 
 zonk_tc_tyvar :: (TcTyVar -> TcM Type)         -- What to do for an unbound mutable variable
              -> TcTyVar -> TcM TcType
@@ -593,35 +615,20 @@ zonk_tc_tyvar unbound_var_fn tyvar
 %************************************************************************
 
 \begin{code}
-readKindVar  :: KindVar -> TcM (Maybe TcKind)
+readKindVar  :: KindVar -> TcM (MetaDetails)
 writeKindVar :: KindVar -> TcKind -> TcM ()
 readKindVar  kv = readMutVar (kindVarRef kv)
-writeKindVar kv val = writeMutVar (kindVarRef kv) (Just val)
+writeKindVar kv val = writeMutVar (kindVarRef kv) (Indirect val)
 
 -------------
 zonkTcKind :: TcKind -> TcM TcKind
-zonkTcKind (FunKind k1 k2) = do { k1' <- zonkTcKind k1
-                               ; k2' <- zonkTcKind k2
-                               ; returnM (FunKind k1' k2') }
-zonkTcKind k@(KindVar kv) = do { mb_kind <- readKindVar kv 
-                              ; case mb_kind of
-                                   Nothing -> returnM k
-                                   Just k  -> zonkTcKind k }
-zonkTcKind other_kind = returnM other_kind
+zonkTcKind k = zonkTcType k
 
 -------------
 zonkTcKindToKind :: TcKind -> TcM Kind
-zonkTcKindToKind (FunKind k1 k2) = do { k1' <- zonkTcKindToKind k1
-                                     ; k2' <- zonkTcKindToKind k2
-                                     ; returnM (FunKind k1' k2') }
-
-zonkTcKindToKind (KindVar kv) = do { mb_kind <- readKindVar kv 
-                                  ; case mb_kind of
-                                      Nothing -> return liftedTypeKind
-                                      Just k  -> zonkTcKindToKind k }
-
-zonkTcKindToKind OpenTypeKind = returnM liftedTypeKind -- An "Open" kind defaults to *
-zonkTcKindToKind other_kind   = returnM other_kind
+-- When zonking a TcKind to a kind, we need to instantiate kind variables,
+-- Haskell specifies that * is to be used, so we follow that.
+zonkTcKindToKind k = zonkType (\ _ -> return liftedTypeKind) k
 \end{code}
                        
 %************************************************************************
@@ -686,11 +693,11 @@ checkValidType ctxt ty
 
        kind_ok = case ctxt of
                        TySynCtxt _  -> True    -- Any kind will do
-                       ResSigCtxt   -> isOpenTypeKind   actual_kind
-                       ExprSigCtxt  -> isOpenTypeKind   actual_kind
+                       ResSigCtxt   -> isSubOpenTypeKind        actual_kind
+                       ExprSigCtxt  -> isSubOpenTypeKind        actual_kind
                        GenPatCtxt   -> isLiftedTypeKind actual_kind
                        ForSigCtxt _ -> isLiftedTypeKind actual_kind
-                       other        -> isArgTypeKind    actual_kind
+                       other        -> isSubArgTypeKind    actual_kind
        
        ubx_tup | not gla_exts = UT_NotOk
                | otherwise    = case ctxt of
@@ -776,7 +783,7 @@ check_tau_type rank ubx_tup ty@(FunTy (PredTy _) _) = failWithTc (forAllTyErr ty
 -- 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_tau_type rank ubx_tup (PredTy sty) = getDOpts            `thenM` \ dflags ->
-                                          check_source_ty dflags TypeCtxt sty
+                                          check_pred_ty dflags TypeCtxt sty
 
 check_tau_type rank ubx_tup (TyVarTy _)       = returnM ()
 check_tau_type rank ubx_tup ty@(FunTy arg_ty res_ty)
@@ -888,12 +895,12 @@ check_valid_theta ctxt []
 check_valid_theta ctxt theta
   = getDOpts                                   `thenM` \ dflags ->
     warnTc (notNull dups) (dupPredWarn dups)   `thenM_`
-    mappM_ (check_source_ty dflags ctxt) theta
+    mappM_ (check_pred_ty dflags ctxt) theta
   where
     (_,dups) = removeDups tcCmpPred theta
 
 -------------------------
-check_source_ty dflags ctxt pred@(ClassP cls tys)
+check_pred_ty dflags ctxt pred@(ClassP cls tys)
   =    -- Class predicates are valid in all contexts
     checkTc (arity == n_tys) arity_err         `thenM_`
 
@@ -909,7 +916,7 @@ check_source_ty dflags ctxt pred@(ClassP cls tys)
     arity_err  = arityErr "Class" class_name arity n_tys
     how_to_allow = parens (ptext SLIT("Use -fglasgow-exts to permit this"))
 
-check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
+check_pred_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- Implicit parameters only allows in type
        -- signatures; not in instance decls, superclasses etc
        -- The reason for not allowing implicit params in instances is a bit subtle
@@ -920,7 +927,7 @@ check_source_ty dflags SigmaCtxt (IParam _ ty) = check_arg_type ty
        -- instance decl would show up two uses of ?x.
 
 -- Catch-all
-check_source_ty dflags ctxt sty = failWithTc (badSourceTyErr sty)
+check_pred_ty dflags ctxt sty = failWithTc (badPredTyErr sty)
 
 -------------------------
 check_class_pred_tys dflags ctxt tys 
@@ -1024,7 +1031,7 @@ checkThetaCtxt ctxt theta
   = vcat [ptext SLIT("In the context:") <+> pprTheta theta,
          ptext SLIT("While checking") <+> pprSourceTyCtxt ctxt ]
 
-badSourceTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
+badPredTyErr sty = ptext SLIT("Illegal constraint") <+> pprPred sty
 predTyVarErr pred  = sep [ptext SLIT("Non type-variable argument"),
                          nest 2 (ptext SLIT("in the constraint:") <+> pprPred pred)]
 dupPredWarn dups   = ptext SLIT("Duplicate constraint(s):") <+> pprWithCommas pprPred (map head dups)
@@ -1184,6 +1191,7 @@ fvTypes tys                = concat (map fvType tys)
 fvPred :: PredType -> [TyVar]
 fvPred (ClassP _ tys')     = fvTypes tys'
 fvPred (IParam _ ty)       = fvType ty
+fvPred (EqPred ty1 ty2)    = fvType ty1 ++ fvType ty2
 
 -- Size of a type: the number of variables and constructors
 sizeType :: Type -> Int
@@ -1202,4 +1210,5 @@ sizeTypes xs               = sum (map sizeType xs)
 sizePred :: PredType -> Int
 sizePred (ClassP _ tys')   = sizeTypes tys'
 sizePred (IParam _ ty)     = sizeType ty
+sizePred (EqPred ty1 ty2)  = sizeType ty1 + sizeType ty2
 \end{code}
index 27d1e9b..61faca8 100644 (file)
@@ -6,7 +6,7 @@
 \begin{code}
 module TcMatches ( tcMatchesFun, tcGRHSsPat, tcMatchesCase, tcMatchLambda,
                   matchCtxt, TcMatchCtxt(..), 
-                  tcStmts, tcDoStmts, 
+                  tcStmts, tcDoStmts, tcBody,
                   tcDoStmt, tcMDoStmt, tcGuardStmt
        ) where
 
@@ -16,16 +16,18 @@ import {-# SOURCE #-}       TcExpr( tcSyntaxOp, tcInferRho, tcMonoExpr, tcPolyExpr )
 
 import HsSyn           ( HsExpr(..), LHsExpr, MatchGroup(..),
                          Match(..), LMatch, GRHSs(..), GRHS(..), 
-                         Stmt(..), LStmt, HsMatchContext(..), HsStmtContext(..),
+                         Stmt(..), LStmt, HsMatchContext(..),
+                         HsStmtContext(..), 
                          pprMatch, isIrrefutableHsPat, mkHsCoerce,
-                         pprMatchContext, pprStmtContext, 
+                         mkLHsCoerce, pprMatchContext, pprStmtContext,  
                          noSyntaxExpr, matchGroupArity, pprMatches,
                          ExprCoFn )
 
 import TcRnMonad
+import TcGadt          ( Refinement, emptyRefinement, refineResType )
 import Inst            ( newMethodFromName )
 import TcEnv           ( TcId, tcLookupLocalIds, tcLookupId, tcExtendIdEnv )
-import TcPat           ( PatCtxt(..), tcPats, tcPat )
+import TcPat           ( tcLamPats, tcLamPat )
 import TcMType         ( newFlexiTyVarTy, newFlexiTyVarTys ) 
 import TcType          ( TcType, TcRhoType, 
                          BoxySigmaType, BoxyRhoType, 
@@ -42,7 +44,6 @@ import Id             ( idType, mkLocalId )
 import TyCon           ( TyCon )
 import Outputable
 import SrcLoc          ( Located(..), getLoc )
-import ErrUtils                ( Message )
 \end{code}
 
 %************************************************************************
@@ -85,7 +86,7 @@ tcMatchesFun fun_name matches exp_ty
     doc = ptext SLIT("The equation(s) for") <+> quotes (ppr fun_name)
          <+> ptext SLIT("have") <+> speakNOf n_pats (ptext SLIT("argument"))
     n_pats = matchGroupArity matches
-    match_ctxt = MC { mc_what = FunRhs fun_name, mc_body = tcPolyExpr }
+    match_ctxt = MC { mc_what = FunRhs fun_name, mc_body = tcBody }
 \end{code}
 
 @tcMatchesCase@ doesn't do the argument-count check because the
@@ -112,17 +113,19 @@ tcMatchLambda match res_ty
                        -- The pprSetDepth makes the abstraction print briefly
                ptext SLIT("has") <+> speakNOf n_pats (ptext SLIT("argument"))]
     match_ctxt = MC { mc_what = LambdaExpr,
-                     mc_body = tcPolyExpr }
+                     mc_body = tcBody }
 \end{code}
 
 @tcGRHSsPat@ typechecks @[GRHSs]@ that occur in a @PatMonoBind@.
 
 \begin{code}
 tcGRHSsPat :: GRHSs Name -> BoxyRhoType -> TcM (GRHSs TcId)
-tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss res_ty
+-- Used for pattern bindings
+tcGRHSsPat grhss res_ty = tcGRHSs match_ctxt grhss (emptyRefinement, res_ty)
+                       -- emptyRefinement: no refinement in a pattern binding
   where
     match_ctxt = MC { mc_what = PatBindRhs,
-                     mc_body = tcPolyExpr }
+                     mc_body = tcBody }
 \end{code}
 
 
@@ -142,7 +145,7 @@ tcMatches :: TcMatchCtxt
 data TcMatchCtxt       -- c.f. TcStmtCtxt, also in this module
   = MC { mc_what :: HsMatchContext Name,       -- What kind of thing this is
         mc_body :: LHsExpr Name                -- Type checker for a body of an alternative
-                -> BoxyRhoType 
+                -> (Refinement, BoxyRhoType) 
                 -> TcM (LHsExpr TcId) }        
 
 tcMatches ctxt pat_tys rhs_ty (MatchGroup matches _)
@@ -161,7 +164,7 @@ tcMatch ctxt pat_tys rhs_ty match
   where
     tc_match ctxt pat_tys rhs_ty match@(Match pats maybe_rhs_sig grhss)
       = addErrCtxt (matchCtxt (mc_what ctxt) match)    $       
-        do { (pats', grhss') <- tcPats LamPat pats pat_tys rhs_ty $
+        do { (pats', grhss') <- tcLamPats pats pat_tys rhs_ty $
                                tc_grhss ctxt maybe_rhs_sig grhss
           ; return (Match pats' Nothing grhss') }
 
@@ -169,13 +172,14 @@ tcMatch ctxt pat_tys rhs_ty match
       = tcGRHSs ctxt grhss rhs_ty      -- No result signature
 
        -- Result type sigs are no longer supported
-    tc_grhss ctxt (Just res_sig) grhss rhs_ty 
+    tc_grhss ctxt (Just res_sig) grhss (co,rhs_ty)
       = do { addErr (ptext SLIT("Ignoring (deprecated) result type signature")
                        <+> ppr res_sig)
-          ; tcGRHSs ctxt grhss rhs_ty }
+            tcGRHSs ctxt grhss (co, inner_ty) }
 
 -------------
-tcGRHSs :: TcMatchCtxt -> GRHSs Name -> BoxyRhoType -> TcM (GRHSs TcId)
+tcGRHSs :: TcMatchCtxt -> GRHSs Name -> (Refinement, BoxyRhoType) 
+       -> TcM (GRHSs TcId)
 
 -- Notice that we pass in the full res_ty, so that we get
 -- good inference from simple things like
@@ -190,7 +194,7 @@ tcGRHSs ctxt (GRHSs grhss binds) res_ty
        ; returnM (GRHSs grhss' binds') }
 
 -------------
-tcGRHS :: TcMatchCtxt -> BoxyRhoType -> GRHS Name -> TcM (GRHS TcId)
+tcGRHS :: TcMatchCtxt -> (Refinement, BoxyRhoType) -> GRHS Name -> TcM (GRHS TcId)
 
 tcGRHS ctxt res_ty (GRHS guards rhs)
   = do  { (guards', rhs') <- tcStmts stmt_ctxt tcGuardStmt guards res_ty $
@@ -215,21 +219,24 @@ tcDoStmts :: HsStmtContext Name
          -> TcM (HsExpr TcId)          -- Returns a HsDo
 tcDoStmts ListComp stmts body res_ty
   = do { elt_ty <- boxySplitListTy res_ty
-       ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts elt_ty $
-                            tcBody (doBodyCtxt ListComp body) body
+       ; (stmts', body') <- tcStmts ListComp (tcLcStmt listTyCon) stmts 
+                                    (emptyRefinement,elt_ty) $
+                            tcBody body
        ; return (HsDo ListComp stmts' body' (mkListTy elt_ty)) }
 
 tcDoStmts PArrComp stmts body res_ty
   = do { [elt_ty] <- boxySplitTyConApp parrTyCon res_ty
-       ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts elt_ty $
-                            tcBody (doBodyCtxt PArrComp body) body
+       ; (stmts', body') <- tcStmts PArrComp (tcLcStmt parrTyCon) stmts 
+                                    (emptyRefinement, elt_ty) $
+                            tcBody body
        ; return (HsDo PArrComp stmts' body' (mkPArrTy elt_ty)) }
 
 tcDoStmts DoExpr stmts body res_ty
   = do { (m_ty, elt_ty) <- boxySplitAppTy res_ty
        ; let res_ty' = mkAppTy m_ty elt_ty     -- The boxySplit consumes res_ty
-       ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts res_ty' $
-                            tcBody (doBodyCtxt DoExpr body) body
+       ; (stmts', body') <- tcStmts DoExpr (tcDoStmt m_ty) stmts 
+                                    (emptyRefinement, res_ty') $
+                            tcBody body
        ; return (HsDo DoExpr stmts' body' res_ty') }
 
 tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
@@ -238,8 +245,9 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
              tc_rhs rhs = withBox liftedTypeKind $ \ pat_ty ->
                           tcMonoExpr rhs (mkAppTy m_ty pat_ty)
 
-       ; (stmts', body') <- tcStmts ctxt (tcMDoStmt tc_rhs) stmts res_ty' $
-                            tcBody (doBodyCtxt ctxt body) body
+       ; (stmts', body') <- tcStmts ctxt (tcMDoStmt tc_rhs) stmts 
+                                    (emptyRefinement, res_ty') $
+                            tcBody body
 
        ; let names = [mfixName, bindMName, thenMName, returnMName, failMName]
        ; insts <- mapM (newMethodFromName DoOrigin m_ty) names
@@ -247,10 +255,12 @@ tcDoStmts ctxt@(MDoExpr _) stmts body res_ty
 
 tcDoStmts ctxt stmts body res_ty = pprPanic "tcDoStmts" (pprStmtContext ctxt)
 
-tcBody :: Message -> LHsExpr Name -> BoxyRhoType -> TcM (LHsExpr TcId)
-tcBody ctxt body res_ty
-  = -- addErrCtxt ctxt $       -- This context adds little that is useful
-    tcPolyExpr body res_ty
+tcBody :: LHsExpr Name -> (Refinement, BoxyRhoType) -> TcM (LHsExpr TcId)
+tcBody body (reft, res_ty)
+  = do { traceTc (text "tcBody" <+> ppr res_ty <+> ppr reft)
+       ; let (co, res_ty') = refineResType reft res_ty
+       ; body' <- tcPolyExpr body res_ty'
+       ; return (mkLHsCoerce co body') } 
 \end{code}
 
 
@@ -262,11 +272,11 @@ tcBody ctxt body res_ty
 
 \begin{code}
 type TcStmtChecker
-  = forall thing.  HsStmtContext Name
-                  -> Stmt Name
-                  -> BoxyRhoType                       -- Result type for comprehension
-                  -> (BoxyRhoType -> TcM thing)        -- Checker for what follows the stmt
-                  -> TcM (Stmt TcId, thing)
+  =  forall thing. HsStmtContext Name
+               -> Stmt Name
+               -> (Refinement, BoxyRhoType)                    -- Result type for comprehension
+               -> ((Refinement,BoxyRhoType) -> TcM thing)      -- Checker for what follows the stmt
+               -> TcM (Stmt TcId, thing)
 
   -- The incoming BoxyRhoType may be refined by type refinements
   -- before being passed to the thing_inside
@@ -274,8 +284,8 @@ type TcStmtChecker
 tcStmts :: HsStmtContext Name
        -> TcStmtChecker        -- NB: higher-rank type
         -> [LStmt Name]
-       -> BoxyRhoType
-       -> (BoxyRhoType -> TcM thing)
+       -> (Refinement, BoxyRhoType)
+       -> ((Refinement, BoxyRhoType) -> TcM thing)
         -> TcM ([LStmt TcId], thing)
 
 -- Note the higher-rank type.  stmt_chk is applied at different
@@ -312,7 +322,7 @@ tcGuardStmt ctxt (ExprStmt guard _ _) res_ty thing_inside
 
 tcGuardStmt ctxt (BindStmt pat rhs _ _) res_ty thing_inside
   = do { (rhs', rhs_ty) <- tcInferRho rhs
-       ; (pat', thing)  <- tcPat LamPat pat rhs_ty res_ty thing_inside
+       ; (pat', thing)  <- tcLamPat pat rhs_ty res_ty thing_inside
        ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
 tcGuardStmt ctxt stmt res_ty thing_inside
@@ -329,7 +339,7 @@ tcLcStmt :: TyCon   -- The list/Parray type constructor ([] or PArray)
 tcLcStmt m_tc ctxt (BindStmt pat rhs _ _) res_ty thing_inside 
  = do  { (rhs', pat_ty) <- withBox liftedTypeKind $ \ ty ->
                            tcMonoExpr rhs (mkTyConApp m_tc [ty])
-       ; (pat', thing)  <- tcPat LamPat pat pat_ty res_ty thing_inside
+       ; (pat', thing)  <- tcLamPat pat pat_ty res_ty thing_inside
        ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
 -- A boolean guard
@@ -385,7 +395,7 @@ tcLcStmt m_tc ctxt stmt elt_ty thing_inside
 tcDoStmt :: TcType             -- Monad type,  m
         -> TcStmtChecker
 
-tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
+tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) reft_res_ty@(_,res_ty) thing_inside
   = do { (rhs', pat_ty) <- withBox liftedTypeKind $ \ pat_ty -> 
                            tcMonoExpr rhs (mkAppTy m_ty pat_ty)
                -- We should use type *inference* for the RHS computations, becuase of GADTs. 
@@ -395,7 +405,7 @@ tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
                -- We do inference on rhs, so that information about its type can be refined
                -- when type-checking the pattern. 
 
-       ; (pat', thing) <- tcPat LamPat pat pat_ty res_ty thing_inside
+       ; (pat', thing) <- tcLamPat pat pat_ty reft_res_ty thing_inside
 
        -- Deal with rebindable syntax; (>>=) :: m a -> (a -> m b) -> m b
        ; let bind_ty = mkFunTys [mkAppTy m_ty pat_ty, 
@@ -409,14 +419,14 @@ tcDoStmt m_ty ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
        ; return (BindStmt pat' rhs' bind_op' fail_op', thing) }
 
 
-tcDoStmt m_ty ctxt (ExprStmt rhs then_op _) res_ty thing_inside
+tcDoStmt m_ty ctxt (ExprStmt rhs then_op _) reft_res_ty@(_,res_ty) thing_inside
   = do {       -- Deal with rebindable syntax; (>>) :: m a -> m b -> m b
          a_ty <- newFlexiTyVarTy liftedTypeKind
        ; let rhs_ty  = mkAppTy m_ty a_ty
              then_ty = mkFunTys [rhs_ty, res_ty] res_ty
        ; then_op' <- tcSyntaxOp DoOrigin then_op then_ty
        ; rhs' <- tcPolyExpr rhs rhs_ty
-       ; thing <- thing_inside res_ty
+       ; thing <- thing_inside reft_res_ty
        ; return (ExprStmt rhs' then_op' rhs_ty, thing) }
 
 tcDoStmt m_ty ctxt stmt res_ty thing_inside
@@ -432,7 +442,7 @@ tcMDoStmt :: (LHsExpr Name -> TcM (LHsExpr TcId, TcType))   -- RHS inference
          -> TcStmtChecker
 tcMDoStmt tc_rhs ctxt (BindStmt pat rhs bind_op fail_op) res_ty thing_inside
   = do { (rhs', pat_ty) <- tc_rhs rhs
-       ; (pat', thing)  <- tcPat LamPat pat pat_ty res_ty thing_inside
+       ; (pat', thing)  <- tcLamPat pat pat_ty res_ty thing_inside
        ; return (BindStmt pat' rhs' noSyntaxExpr noSyntaxExpr, thing) }
 
 tcMDoStmt tc_rhs ctxt (ExprStmt rhs then_op _) res_ty thing_inside
@@ -506,10 +516,6 @@ checkArgs fun other = panic "TcPat.checkArgs"      -- Matches always non-empty
 matchCtxt ctxt match  = hang (ptext SLIT("In") <+> pprMatchContext ctxt <> colon) 
                           4 (pprMatch ctxt match)
 
-doBodyCtxt :: HsStmtContext Name -> LHsExpr Name -> SDoc
-doBodyCtxt ctxt body = hang (ptext SLIT("In the result of") <+> pprStmtContext ctxt <> colon) 
-                         4 (ppr body)
-
 stmtCtxt ctxt stmt = hang (ptext SLIT("In") <+> pprStmtContext ctxt <> colon)
                        4 (ppr stmt)
 \end{code}
index 56c5258..33b7630 100644 (file)
@@ -4,13 +4,14 @@
 \section[TcPat]{Typechecking patterns}
 
 \begin{code}
-module TcPat ( tcPat, tcPats, tcOverloadedLit,
-              PatCtxt(..), badFieldCon, polyPatSig ) where
+module TcPat ( tcLetPat, tcLamPat, tcLamPats, tcOverloadedLit,
+              badFieldCon, polyPatSig ) where
 
 #include "HsVersions.h"
 
 import {-# SOURCE #-}  TcExpr( tcSyntaxOp )
 import HsSyn           ( Pat(..), LPat, HsConDetails(..), HsLit(..), HsOverLit(..), HsExpr(..),
+                         mkCoPat, idCoercion,
                          LHsBinds, emptyLHsBinds, isEmptyLHsBinds, 
                          collectPatsBinders, nlHsLit )
 import TcHsSyn         ( TcId, hsLitType )
@@ -23,35 +24,37 @@ import CoreFVs              ( idFreeTyVars )
 import Name            ( Name, mkSystemVarName )
 import TcSimplify      ( tcSimplifyCheck, bindInstsOfLocalFuns )
 import TcEnv           ( newLocalName, tcExtendIdEnv1, tcExtendTyVarEnv2,
-                         tcLookupClass, tcLookupDataCon, tcLookupId, refineEnvironment,
-                         tcMetaTy )
-import TcMType                 ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, newBoxyTyVar, zonkTcType )
+                         tcLookupClass, tcLookupDataCon, refineEnvironment,
+                         tcLookupField, tcMetaTy )
+import TcMType                 ( newFlexiTyVarTy, arityErr, tcInstSkolTyVars, 
++                        newCoVars, zonkTcType )
 import TcType          ( TcType, TcTyVar, TcSigmaType, TcRhoType, BoxyType,
                          SkolemInfo(PatSkol), 
                          BoxySigmaType, BoxyRhoType, argTypeKind, typeKind,
-                         pprSkolTvBinding, isRefineableTy, isRigidTy, tcTyVarsOfTypes, mkTyVarTy, lookupTyVar, 
-                         emptyTvSubst, substTyVar, substTy, mkTopTvSubst, zipTopTvSubst, zipOpenTvSubst,
-                         mkTyVarTys, mkClassPred, mkTyConApp, isOverloadedTy, isArgTypeKind, isUnboxedTupleType,
-                         mkFunTy, mkFunTys, exactTyVarsOfTypes, tidyOpenType, tidyOpenTypes )
-import VarSet          ( elemVarSet, mkVarSet )
-import Kind            ( liftedTypeKind, openTypeKind )
-import TcUnify         ( boxySplitTyConApp, boxySplitListTy, unifyType,
-                         unBox, stripBoxyType, zapToMonotype,
-                         boxyMatchTypes, boxyUnify, boxyUnifyList, checkSigTyVarsWrt )
+                         pprSkolTvBinding, isRigidTy, tcTyVarsOfTypes, 
+                         zipTopTvSubst, isArgTypeKind, isUnboxedTupleType,
+                         mkTyVarTys, mkClassPred, isOverloadedTy, substEqSpec,
+                         mkFunTy, mkFunTys, tidyOpenType, tidyOpenTypes )
+import VarSet          ( elemVarSet )
+import {- Kind parts of -} 
+       Type            ( liftedTypeKind )
+import TcUnify         ( boxySplitTyConApp, boxySplitListTy, unBox,
+                         zapToMonotype, boxyUnify, checkSigTyVarsWrt,
+                         unifyType )
 import TcHsType                ( UserTypeCtxt(..), tcPatSig )
 import TysWiredIn      ( boolTy, parrTyCon, tupleTyCon )
-import Unify           ( MaybeErr(..), gadtRefineTys )
 import Type            ( substTys, substTheta )
 import StaticFlags     ( opt_IrrefutableTuples )
-import TyCon           ( TyCon )
-import DataCon         ( DataCon, dataConTyCon, isVanillaDataCon, 
-                         dataConFieldLabels, dataConSourceArity, dataConSig )
+import TyCon           ( TyCon, FieldLabel )
+import DataCon         ( DataCon, dataConTyCon, dataConFullSig, dataConName,
+                         dataConFieldLabels, dataConSourceArity )
 import PrelNames       ( integralClassName, fromIntegerName, integerTyConName, 
                          fromRationalName, rationalTyConName )
 import BasicTypes      ( isBoxed )
 import SrcLoc          ( Located(..), SrcSpan, noLoc )
 import ErrUtils                ( Message )
-import Util            ( takeList, zipEqual )
+import Util            ( zipEqual )
+import Maybes          ( MaybeErr(..) )
 import Outputable
 import FastString
 \end{code}
@@ -64,12 +67,26 @@ import FastString
 %************************************************************************
 
 \begin{code}
-tcPats :: PatCtxt
-       -> [LPat Name]                  -- Patterns,
-       -> [BoxySigmaType]              --   and their types
-       -> BoxyRhoType                  -- Result type,
-       -> (BoxyRhoType -> TcM a)       --   and the checker for the body
-       -> TcM ([LPat TcId], a)
+tcLetPat :: (Name -> Maybe TcRhoType)
+        -> LPat Name -> BoxySigmaType 
+        -> TcM a
+        -> TcM (LPat TcId, a)
+tcLetPat sig_fn pat pat_ty thing_inside
+  = do { let init_state = PS { pat_ctxt = LetPat sig_fn, 
+                               pat_reft = emptyRefinement }
+       ; (pat', ex_tvs, res) <- tc_lpat pat pat_ty init_state (\ _ -> thing_inside)
+
+       -- Don't know how to deal with pattern-bound existentials yet
+       ; checkTc (null ex_tvs) (existentialExplode pat)
+
+       ; return (pat', res) }
+
+-----------------
+tcLamPats :: [LPat Name]                               -- Patterns,
+         -> [BoxySigmaType]                            --   and their types
+         -> BoxyRhoType                                -- Result type,
+         -> ((Refinement, BoxyRhoType) -> TcM a)       --   and the checker for the body
+         -> TcM ([LPat TcId], a)
 
 -- This is the externally-callable wrapper function
 -- Typecheck the patterns, extend the environment to bind the variables,
@@ -79,36 +96,42 @@ tcPats      :: PatCtxt
 
 --   1. Initialise the PatState
 --   2. Check the patterns
---   3. Apply the refinement
+--   3. Apply the refinement to the environment and result type
 --   4. Check the body
 --   5. Check that no existentials escape
 
-tcPats ctxt pats tys res_ty thing_inside
-  =  do        { let init_state = PS { pat_ctxt = ctxt, pat_reft = emptyTvSubst }
+tcLamPats pats tys res_ty thing_inside
+  = tc_lam_pats (zipEqual "tcLamPats" pats tys)
+               (emptyRefinement, res_ty) thing_inside
+
+tcLamPat :: LPat Name -> BoxySigmaType 
+        -> (Refinement,BoxyRhoType)            -- Result type
+        -> ((Refinement,BoxyRhoType) -> TcM a) -- Checker for body, given its result type
+        -> TcM (LPat TcId, a)
+tcLamPat pat pat_ty res_ty thing_inside
+  = do { ([pat'],thing) <- tc_lam_pats [(pat, pat_ty)] res_ty thing_inside
+       ; return (pat', thing) }
 
-       ; (pats', ex_tvs, res) <- tc_lpats init_state pats tys $ \ pstate' ->
+-----------------
+tc_lam_pats :: [(LPat Name,BoxySigmaType)]
+                   -> (Refinement,BoxyRhoType)                 -- Result type
+                   -> ((Refinement,BoxyRhoType) -> TcM a)      -- Checker for body, given its result type
+                   -> TcM ([LPat TcId], a)
+tc_lam_pats pat_ty_prs (reft, res_ty) thing_inside 
+  =  do        { let init_state = PS { pat_ctxt = LamPat, pat_reft = reft }
+
+       ; (pats', ex_tvs, res) <- tcMultiple tc_lpat_pr pat_ty_prs init_state $ \ pstate' ->
                                  refineEnvironment (pat_reft pstate') $
-                                 thing_inside (refineType (pat_reft pstate') res_ty)
+                                 thing_inside (pat_reft pstate', res_ty)
 
-       ; tcCheckExistentialPat ctxt pats' ex_tvs tys res_ty
+       ; let tys = map snd pat_ty_prs
+       ; tcCheckExistentialPat pats' ex_tvs tys res_ty
 
        ; returnM (pats', res) }
 
 
 -----------------
-tcPat :: PatCtxt 
-      -> LPat Name -> BoxySigmaType 
-      -> BoxyRhoType           -- Result type
-      -> (BoxyRhoType -> TcM a)        -- Checker for body, given its result type
-      -> TcM (LPat TcId, a)
-tcPat ctxt pat pat_ty res_ty thing_inside
-  = do { ([pat'],thing) <- tcPats ctxt [pat] [pat_ty] res_ty thing_inside
-       ; return (pat', thing) }
-
-
------------------
-tcCheckExistentialPat :: PatCtxt
-                     -> [LPat TcId]            -- Patterns (just for error message)
+tcCheckExistentialPat :: [LPat TcId]           -- Patterns (just for error message)
                      -> [TcTyVar]              -- Existentially quantified tyvars bound by pattern
                      -> [BoxySigmaType]        -- Types of the patterns
                      -> BoxyRhoType            -- Type of the body of the match
@@ -120,20 +143,16 @@ tcCheckExistentialPat :: PatCtxt
 --     f (C g) x = g x
 -- Here, result_ty will be simply Int, but expected_ty is (C -> a -> Int).
 
-tcCheckExistentialPat ctxt pats [] pat_tys body_ty
+tcCheckExistentialPat pats [] pat_tys body_ty
   = return ()  -- Short cut for case when there are no existentials
 
-tcCheckExistentialPat (LetPat _) pats ex_tvs pat_tys body_ty
-       -- Don't know how to deal with pattern-bound existentials yet
-  = failWithTc (existentialExplode pats)
-
-tcCheckExistentialPat ctxt pats ex_tvs pat_tys body_ty
+tcCheckExistentialPat pats ex_tvs pat_tys body_ty
   = addErrCtxtM (sigPatCtxt (collectPatsBinders pats) ex_tvs pat_tys body_ty)  $
     checkSigTyVarsWrt (tcTyVarsOfTypes (body_ty:pat_tys)) ex_tvs
 
 data PatState = PS {
        pat_ctxt :: PatCtxt,
-       pat_reft :: GadtRefinement      -- Binds rigid TcTyVars to their refinements
+       pat_reft :: Refinement  -- Binds rigid TcTyVars to their refinements
   }
 
 data PatCtxt 
@@ -235,46 +254,57 @@ Hence the getErrCtxt/setErrCtxt stuff in tc_lpats.
 
 \begin{code}
 --------------------
-tc_lpats :: PatState
-        -> [LPat Name] 
-        -> [BoxySigmaType]     
-        -> (PatState -> TcM a)
-        -> TcM ([LPat TcId], [TcTyVar], a)
-
-tc_lpats pstate pats pat_tys thing_inside
+type Checker inp out =  forall r.
+                         inp
+                      -> PatState
+                      -> (PatState -> TcM r)
+                      -> TcM (out, [TcTyVar], r)
+
+tcMultiple :: Checker inp out -> Checker [inp] [out]
+tcMultiple tc_pat args pstate thing_inside
   = do { err_ctxt <- getErrCtxt
-       ; let loop pstate [] [] 
+       ; let loop pstate []
                = do { res <- thing_inside pstate
                     ; return ([], [], res) }
 
-             loop pstate (p:ps) (ty:tys)
+             loop pstate (arg:args)
                = do { (p', p_tvs, (ps', ps_tvs, res)) 
-                               <- tc_lpat pstate p ty $ \ pstate' ->
+                               <- tc_pat arg pstate $ \ pstate' ->
                                   setErrCtxt err_ctxt $
-                                  loop pstate' ps tys
+                                  loop pstate' args
                -- setErrCtxt: restore context before doing the next pattern
                -- See note [Nesting] above
                                
                     ; return (p':ps', p_tvs ++ ps_tvs, res) }
 
-             loop _ _ _ = pprPanic "tc_lpats" (ppr pats $$ ppr pat_tys)
-
-       ; loop pstate pats pat_tys }
+       ; loop pstate args }
 
 --------------------
-tc_lpat :: PatState
-        -> LPat Name 
-        -> BoxySigmaType
-        -> (PatState -> TcM a)
-        -> TcM (LPat TcId, [TcTyVar], a)
-tc_lpat pstate (L span pat) pat_ty thing_inside
+tc_lpat_pr :: (LPat Name, BoxySigmaType)
+          -> PatState
+          -> (PatState -> TcM a)
+          -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat_pr (pat, ty) = tc_lpat pat ty
+
+tc_lpat :: LPat Name 
+       -> BoxySigmaType
+       -> PatState
+       -> (PatState -> TcM a)
+       -> TcM (LPat TcId, [TcTyVar], a)
+tc_lpat (L span pat) pat_ty pstate thing_inside
   = setSrcSpan span              $
     maybeAddErrCtxt (patCtxt pat) $
-    do { let pat_ty' = refineType (pat_reft pstate) pat_ty
+    do { let (coercion, pat_ty') = refineType (pat_reft pstate) pat_ty
                -- Make sure the result type reflects the current refinement
-       ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
-       ; return (L span pat', tvs, res) }
+               -- We must do this here, so that it correctly ``sees'' all
+               -- the refinements to the left.  Example:
+               -- Suppose C :: forall a. T a -> a -> Foo
+               -- Pattern      C a p1 True
+               -- So p1 might refine 'a' to True, and the True 
+               -- pattern had better see it.
 
+       ; (pat', tvs, res) <- tc_pat pstate pat pat_ty' thing_inside
+       ; return (mkCoPat coercion (L span pat') pat_ty, tvs, res) }
 
 --------------------
 tc_pat :: PatState
@@ -295,11 +325,11 @@ tc_pat pstate (VarPat name) pat_ty thing_inside
        ; return (pat', [], res) }
 
 tc_pat pstate (ParPat pat) pat_ty thing_inside
-  = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+  = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
        ; return (ParPat pat', tvs, res) }
 
 tc_pat pstate (BangPat pat) pat_ty thing_inside
-  = do { (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+  = do { (pat', tvs, res) <- tc_lpat pat pat_ty pstate thing_inside
        ; return (BangPat pat', tvs, res) }
 
 -- There's a wrinkle with irrefutable patterns, namely that we
@@ -313,7 +343,7 @@ tc_pat pstate (BangPat pat) pat_ty thing_inside
 -- Nor should a lazy pattern bind any existential type variables
 -- because they won't be in scope when we do the desugaring
 tc_pat pstate lpat@(LazyPat pat) pat_ty thing_inside
-  = do { (pat', pat_tvs, res) <- tc_lpat pstate pat pat_ty $ \ _ ->
+  = do { (pat', pat_tvs, res) <- tc_lpat pat pat_ty pstate $ \ _ ->
                                  thing_inside pstate
                                        -- Ignore refined pstate',
                                        -- revert to pstate
@@ -335,7 +365,7 @@ tc_pat pstate (WildPat _) pat_ty thing_inside
 tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
   = do { bndr_id <- setSrcSpan nm_loc (tcPatBndr pstate name pat_ty)
        ; (pat', tvs, res) <- tcExtendIdEnv1 name bndr_id $
-                             tc_lpat pstate pat (idType bndr_id) thing_inside
+                             tc_lpat pat (idType bndr_id) pstate thing_inside
            -- NB: if we do inference on:
            --          \ (y@(x::forall a. a->a)) = e
            -- we'll fail.  The as-pattern infers a monotype for 'y', which then
@@ -350,7 +380,7 @@ tc_pat pstate (AsPat (L nm_loc name) pat) pat_ty thing_inside
 tc_pat pstate (SigPatIn pat sig_ty) pat_ty thing_inside
   = do { (inner_ty, tv_binds) <- tcPatSig (patSigCtxt pstate) sig_ty pat_ty
        ; (pat', tvs, res) <- tcExtendTyVarEnv2 tv_binds $
-                             tc_lpat pstate pat inner_ty thing_inside
+                             tc_lpat pat inner_ty pstate thing_inside
        ; return (SigPatOut pat' inner_ty, tvs, res) }
 
 tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
@@ -360,20 +390,21 @@ tc_pat pstate pat@(TypePat ty) pat_ty thing_inside
 -- Lists, tuples, arrays
 tc_pat pstate (ListPat pats _) pat_ty thing_inside
   = do { elt_ty <- boxySplitListTy pat_ty
-       ; let elt_tys = takeList pats (repeat elt_ty) 
-       ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside
+       ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+                                               pats pstate thing_inside
        ; return (ListPat pats' elt_ty, pats_tvs, res) }
 
 tc_pat pstate (PArrPat pats _) pat_ty thing_inside
   = do { [elt_ty] <- boxySplitTyConApp parrTyCon pat_ty
-       ; let elt_tys = takeList pats (repeat elt_ty) 
-       ; (pats', pats_tvs, res) <- tc_lpats pstate pats elt_tys thing_inside 
+       ; (pats', pats_tvs, res) <- tcMultiple (\p -> tc_lpat p elt_ty)
+                                               pats pstate thing_inside 
        ; ifM (null pats) (zapToMonotype pat_ty)        -- c.f. ExplicitPArr in TcExpr
        ; return (PArrPat pats' elt_ty, pats_tvs, res) }
 
 tc_pat pstate (TuplePat pats boxity _) pat_ty thing_inside
   = do { arg_tys <- boxySplitTyConApp (tupleTyCon boxity (length pats)) pat_ty
-       ; (pats', pats_tvs, res) <- tc_lpats pstate pats arg_tys thing_inside
+       ; (pats', pats_tvs, res) <- tcMultiple tc_lpat_pr (pats `zip` arg_tys)
+                                              pstate thing_inside
 
        -- Under flag control turn a pattern (x,y,z) into ~(x,y,z)
        -- so that we can experiment with lazy tuple-matching.
@@ -447,118 +478,82 @@ tc_pat _ _other_pat _ _ = panic "tc_pat"         -- DictPat, ConPatOut, SigPatOut, VarP
 %************************************************************************
 
 \begin{code}
+--     Running example:
+-- MkT :: forall a b c. (a:=:[b]) => b -> c -> T a
+--      with scrutinee of type (T ty)
+
 tcConPat :: PatState -> SrcSpan -> DataCon -> TyCon 
         -> BoxySigmaType       -- Type of the pattern
         -> HsConDetails Name (LPat Name) -> (PatState -> TcM a)
         -> TcM (Pat TcId, [TcTyVar], a)
 tcConPat pstate con_span data_con tycon pat_ty arg_pats thing_inside
-  | isVanillaDataCon data_con
-  = do { ty_args <- boxySplitTyConApp tycon pat_ty
-       ; let (tvs, _, arg_tys, _, _) = dataConSig data_con
-             arg_tvs  = exactTyVarsOfTypes arg_tys
-               -- See Note [Silly type synonyms in smart-app] in TcExpr
-               -- for why we must use exactTyVarsOfTypes
-             inst_prs = zipEqual "tcConPat" tvs ty_args
-             subst    = mkTopTvSubst inst_prs
-             arg_tys' = substTys subst arg_tys
-             unconstrained_ty_args = [ty_arg | (tv,ty_arg) <- inst_prs,
-                                               not (tv `elemVarSet` arg_tvs)]
-       ; mapM unBox unconstrained_ty_args      -- Zap these to monotypes
-       ; tcInstStupidTheta data_con ty_args
-       ; traceTc (text "tcConPat" <+> vcat [ppr data_con, ppr ty_args, ppr arg_tys'])
-       ; (arg_pats', tvs, res) <- tcConArgs pstate data_con arg_pats arg_tys' thing_inside
-       ; return (ConPatOut (L con_span data_con) [] [] emptyLHsBinds 
-                           arg_pats' (mkTyConApp tycon ty_args),
-                 tvs, res) }
-
-  | otherwise  -- GADT case
-  = do { ty_args <- boxySplitTyConApp tycon pat_ty
-       ; span <- getSrcSpanM   -- The whole pattern
-
-       -- Instantiate the constructor type variables and result type
-       ; let (tvs, theta, arg_tys, _, res_tys) = dataConSig data_con
-             arg_tvs = exactTyVarsOfTypes arg_tys
-               -- See Note [Silly type synonyms in smart-app] in TcExpr
-               -- for why we must use exactTyVarsOfTypes
+  = do { span <- getSrcSpanM   -- Span for the whole pattern
+       ; let (univ_tvs, ex_tvs, eq_spec, theta, arg_tys) = dataConFullSig data_con
              skol_info = PatSkol data_con span
-             arg_flags = [ tv `elemVarSet` arg_tvs | tv <- tvs ]
-       ; tvs' <- tcInstSkolTyVars skol_info tvs
-       ; let res_tys' = substTys (zipTopTvSubst tvs (mkTyVarTys tvs')) res_tys
-
-       -- Do type refinement!
-       ; traceTc (text "tcGadtPat" <+> vcat [ppr data_con, ppr tvs', ppr res_tys', 
-                                             text "ty-args:" <+> ppr ty_args ])
-       ; refineAlt pstate data_con tvs' arg_flags res_tys' ty_args 
-                       $ \ pstate' tv_tys' -> do
-
-       -- ToDo: arg_tys should be boxy, but I don't think theta' should be,
-       --       or the tv_tys' in the call to tcInstStupidTheta
-       { let tenv'    = zipTopTvSubst tvs tv_tys'
-             theta'   = substTheta tenv' theta
-             arg_tys' = substTys   tenv' arg_tys       -- Boxy types
+
+         -- Instantiate the constructor type variables [a->ty]
+       ; ctxt_res_tys <- boxySplitTyConApp tycon pat_ty
+       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs
+       ; let tenv     = zipTopTvSubst (univ_tvs ++ ex_tvs)
+                                     (ctxt_res_tys ++ mkTyVarTys ex_tvs')
+             eq_spec' = substEqSpec tenv eq_spec
+             theta'   = substTheta  tenv theta
+             arg_tys' = substTys    tenv arg_tys
+
+       ; co_vars <- newCoVars eq_spec' -- Make coercion variables
+       ; pstate' <- refineAlt data_con pstate ex_tvs co_vars pat_ty
 
        ; ((arg_pats', inner_tvs, res), lie_req) <- getLIE $
-               do { tcInstStupidTheta data_con tv_tys'
-                       -- The stupid-theta mentions the newly-bound tyvars, so
-                       -- it must live inside the getLIE, so that the
-                       -- tcSimplifyCheck will apply the type refinement to it
-                  ; tcConArgs pstate' data_con arg_pats arg_tys' thing_inside }
+               tcConArgs data_con arg_tys' arg_pats pstate' thing_inside
 
        ; dicts <- newDicts (SigOrigin skol_info) theta'
-       ; dict_binds <- tcSimplifyCheck doc tvs' dicts lie_req
+       ; dict_binds <- tcSimplifyCheck doc ex_tvs' dicts lie_req
+
+       ; tcInstStupidTheta data_con ctxt_res_tys
 
-       ; return (ConPatOut (L con_span data_con)
-                           tvs' (map instToId dicts) dict_binds
-                           arg_pats' (mkTyConApp tycon ty_args),
-                 tvs' ++ inner_tvs, res) 
-       } }
+       ; return (ConPatOut { pat_con = L con_span data_con, 
+                             pat_tvs = ex_tvs' ++ co_vars,
+                             pat_dicts = map instToId dicts, pat_binds = dict_binds,
+                             pat_args = arg_pats', pat_ty = pat_ty },
+                 ex_tvs' ++ inner_tvs, res) 
+       }
   where
     doc = ptext SLIT("existential context for") <+> quotes (ppr data_con)
 
-tcConArgs :: PatState -> DataCon 
-          -> HsConDetails Name (LPat Name) -> [TcSigmaType]
-          -> (PatState -> TcM a)
-          -> TcM (HsConDetails TcId (LPat Id), [TcTyVar], a)
+tcConArgs :: DataCon -> [TcSigmaType]
+         -> Checker (HsConDetails Name (LPat Name)) (HsConDetails Id (LPat Id))
 
-tcConArgs pstate data_con (PrefixCon arg_pats) arg_tys thing_inside
+tcConArgs data_con arg_tys (PrefixCon arg_pats) pstate thing_inside
   = do { checkTc (con_arity == no_of_args)     -- Check correct arity
                  (arityErr "Constructor" data_con con_arity no_of_args)
-       ; (arg_pats', tvs, res) <- tc_lpats pstate arg_pats arg_tys thing_inside
+       ; let pats_w_tys = zipEqual "tcConArgs" arg_pats arg_tys
+       ; (arg_pats', tvs, res) <- tcMultiple tcConArg pats_w_tys
+                                             pstate thing_inside 
        ; return (PrefixCon arg_pats', tvs, res) }
   where
     con_arity  = dataConSourceArity data_con
     no_of_args = length arg_pats
 
-tcConArgs pstate data_con (InfixCon p1 p2) arg_tys thing_inside
+tcConArgs data_con [arg_ty1,arg_ty2] (InfixCon p1 p2) pstate thing_inside
   = do { checkTc (con_arity == 2)      -- Check correct arity
                  (arityErr "Constructor" data_con con_arity 2)
-       ; ([p1',p2'], tvs, res) <- tc_lpats pstate [p1,p2] arg_tys thing_inside
+       ; ([p1',p2'], tvs, res) <- tcMultiple tcConArg [(p1,arg_ty1),(p2,arg_ty2)]
+                                             pstate thing_inside
        ; return (InfixCon p1' p2', tvs, res) }
   where
     con_arity  = dataConSourceArity data_con
 
-tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
-  = do { (rpats', tvs, res) <- tc_fields pstate rpats thing_inside
+tcConArgs data_con arg_tys (RecCon rpats) pstate thing_inside
+  = do { (rpats', tvs, res) <- tcMultiple tc_field rpats pstate thing_inside
        ; return (RecCon rpats', tvs, res) }
   where
-    tc_fields :: PatState -> [(Located Name, LPat Name)]
-             -> (PatState -> TcM a)
-             -> TcM ([(Located TcId, LPat TcId)], [TcTyVar], a)
-    tc_fields pstate [] thing_inside
-      = do { res <- thing_inside pstate
-          ; return ([], [], res) }
-
-    tc_fields pstate (rpat : rpats) thing_inside
-      =        do { (rpat', tvs1, (rpats', tvs2, res)) 
-               <- tc_field pstate rpat  $ \ pstate' ->
-                  tc_fields pstate' rpats thing_inside
-          ; return (rpat':rpats', tvs1 ++ tvs2, res) }
-
-    tc_field pstate (field_lbl, pat) thing_inside
+    tc_field :: Checker (Located Name, LPat Name) (Located TcId, LPat TcId)
+    tc_field (field_lbl, pat) pstate thing_inside
       = do { (sel_id, pat_ty) <- wrapLocFstM find_field_ty field_lbl
-          ; (pat', tvs, res) <- tc_lpat pstate pat pat_ty thing_inside
+          ; (pat', tvs, res) <- tcConArg (pat, pat_ty) pstate thing_inside
           ; return ((sel_id, pat'), tvs, res) }
 
+    find_field_ty :: FieldLabel -> TcM (Id, TcType)
     find_field_ty field_lbl
        = case [ty | (f,ty) <- field_tys, f == field_lbl] of
 
@@ -577,13 +572,21 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
                -- The normal case, when the field comes from the right constructor
           (pat_ty : extras) -> 
                ASSERT( null extras )
-               do { sel_id <- tcLookupId field_lbl
+               do { sel_id <- tcLookupField field_lbl
                   ; return (sel_id, pat_ty) }
 
+    field_tys :: [(FieldLabel, TcType)]
     field_tys = zip (dataConFieldLabels data_con) arg_tys
        -- Don't use zipEqual! If the constructor isn't really a record, then
        -- dataConFieldLabels will be empty (and each field in the pattern
        -- will generate an error below).
+
+tcConArg :: Checker (LPat Name, BoxySigmaType) (LPat Id)
+tcConArg (arg_pat, arg_ty) pstate thing_inside
+  = tc_lpat arg_pat arg_ty pstate thing_inside
+       -- NB: the tc_lpat will refine pat_ty if necessary
+       --     based on the current pstate, which may include
+       --     refinements from peer argument patterns to the left
 \end{code}
 
 
@@ -594,69 +597,44 @@ tcConArgs pstate data_con (RecCon rpats) arg_tys thing_inside
 %************************************************************************
 
 \begin{code}
-refineAlt :: PatState 
-         -> DataCon            -- For tracing only
-         -> [TcTyVar]          -- Type variables from pattern
-         -> [Bool]             -- Flags indicating which type variables occur
-                               --      in the type of at least one argument
-         -> [TcType]           -- Result types from the pattern
-         -> [BoxySigmaType]    -- Result types from the scrutinee (context)
-         -> (PatState -> [BoxySigmaType] -> TcM a)
-                       -- Possibly-refined existentials
-         -> TcM a
-refineAlt pstate con pat_tvs arg_flags pat_res_tys ctxt_res_tys thing_inside
-  | not (all isRigidTy ctxt_res_tys)
-       -- The context is not a rigid type, so we do no type refinement here.  
-  = do { let arg_tvs = mkVarSet [ tv | (tv, True) <- pat_tvs `zip` arg_flags]
-             subst = boxyMatchTypes arg_tvs pat_res_tys ctxt_res_tys
-             
-             res_tvs = tcTyVarsOfTypes pat_res_tys
-               -- The tvs are (already) all fresh skolems. We need a 
-               -- fresh skolem for each type variable (to bind in the pattern)
-               -- even if it's refined away by the type refinement
-             find_inst tv 
-               | not (tv `elemVarSet` res_tvs)        = return (mkTyVarTy tv)
-               | Just boxy_ty <- lookupTyVar subst tv = return boxy_ty
-               | otherwise                            = do { tv <- newBoxyTyVar openTypeKind
-                                                           ; return (mkTyVarTy tv) }
-       ; pat_tys' <- mapM find_inst pat_tvs
-
-       -- Do the thing inside
-       ; res <- thing_inside pstate pat_tys'
-
-       -- Unbox the types that have been filled in by the thing_inside
-       -- I.e. the ones whose type variables are mentioned in at least one arg
-       ; let strip ty in_arg_tv | in_arg_tv = stripBoxyType ty
-                                | otherwise = return ty
-       ; pat_tys'' <- zipWithM strip pat_tys' arg_flags
-       ; let subst = zipOpenTvSubst pat_tvs pat_tys''
-       ; boxyUnifyList (substTys subst pat_res_tys) ctxt_res_tys
-
-       ; return res }          -- All boxes now filled
-
-  | otherwise  -- The context is rigid, so we can do type refinement
-  = case gadtRefineTys (pat_reft pstate) con pat_tvs pat_res_tys ctxt_res_tys of
-       Failed msg -> failWithTc (inaccessibleAlt msg)
-       Succeeded (new_subst, all_bound_here) 
-         | all_bound_here      -- All the new bindings are for pat_tvs, so no need
-                               -- to refine the environment or pstate
-         -> do  { traceTc trace_msg
-                ; thing_inside pstate pat_tvs' }
-         | otherwise   -- New bindings affect the context, so pass down pstate'.  
-                       -- DO NOT refine the envt, because we might be inside a
-                       -- lazy pattern
-         -> do { traceTc trace_msg
-               ; thing_inside pstate' pat_tvs' }
-         where
-            pat_tvs' = map (substTyVar new_subst) pat_tvs
-            pstate'  = pstate { pat_reft = new_subst }
-            trace_msg = text "refineTypes:match" <+> ppr con <+> ppr new_subst
-
-refineType :: GadtRefinement -> BoxyRhoType -> BoxyRhoType
--- Refine the type if it is rigid
-refineType reft ty
-  | isRefineableTy ty = substTy reft ty
-  | otherwise        = ty
+refineAlt :: DataCon           -- For tracing only
+         -> PatState 
+         -> [TcTyVar]          -- Existentials
+         -> [CoVar]            -- Equational constraints
+         -> BoxySigmaType      -- Pattern type
+         -> TcM PatState
+
+refineAlt con pstate ex_tvs [] pat_ty
+  = return pstate      -- Common case: no equational constraints
+
+refineAlt con pstate ex_tvs co_vars pat_ty
+  | not (isRigidTy pat_ty)
+  = failWithTc (nonRigidMatch con)
+       -- We are matching against a GADT constructor with non-trivial
+       -- constraints, but pattern type is wobbly.  For now we fail.
+       -- We can make sense of this, however:
+       -- Suppose MkT :: forall a b. (a:=:[b]) => b -> T a
+       --      (\x -> case x of { MkT v -> v })
+       -- We can infer that x must have type T [c], for some wobbly 'c'
+       -- and translate to
+       --      (\(x::T [c]) -> case x of
+       --                        MkT b (g::([c]:=:[b])) (v::b) -> v `cast` sym g
+       -- To implement this, we'd first instantiate the equational
+       -- constraints with *wobbly* type variables for the existentials;
+       -- then unify these constraints to make pat_ty the right shape;
+       -- then proceed exactly as in the rigid case
+
+  | otherwise  -- In the rigid case, we perform type refinement
+  = case gadtRefine (pat_reft pstate) ex_tvs co_vars of {
+           Failed msg     -> failWithTc (inaccessibleAlt msg) ;
+           Succeeded reft -> do { traceTc trace_msg
+                                ; return (pstate { pat_reft = reft }) }
+                   -- DO NOT refine the envt right away, because we 
+                   -- might be inside a lazy pattern.  Instead, refine pstate
+               where
+                   
+                   trace_msg = text "refineAlt:match" <+> ppr con <+> ppr reft
+       }
 \end{code}
 
 
@@ -799,11 +777,11 @@ patCtxt pat           = Just (hang (ptext SLIT("In the pattern:"))
 
 -----------------------------------------------
 
-existentialExplode pats
+existentialExplode pat
   = hang (vcat [text "My brain just exploded.",
                text "I can't handle pattern bindings for existentially-quantified constructors.",
                text "In the binding group for"])
-       4 (vcat (map ppr pats))
+       4 (ppr pat)
 
 sigPatCtxt bound_ids bound_tvs pat_tys body_ty tidy_env 
   = do { pat_tys' <- mapM zonkTcType pat_tys
@@ -841,6 +819,10 @@ lazyPatErr pat tvs
     hang (ptext SLIT("A lazy (~) pattern connot bind existential type variables"))
        2 (vcat (map pprSkolTvBinding tvs))
 
+nonRigidMatch con
+  =  hang (ptext SLIT("GADT pattern match in non-rigid context for") <+> quotes (ppr con))
+       2 (ptext SLIT("Tell GHC HQ if you'd like this to unify the context"))
+
 inaccessibleAlt msg
   = hang (ptext SLIT("Inaccessible case alternative:")) 2 msg
 \end{code}
index 9e1bfb9..0a4895f 100644 (file)
@@ -113,7 +113,7 @@ import MkId         ( unsafeCoerceId )
 import TyCon           ( tyConName )
 import TysWiredIn      ( mkListTy, unitTy )
 import IdInfo          ( GlobalIdDetails(..) )
-import Kind            ( Kind )
+import {- Kind parts of -} Type                ( Kind, eqKind )
 import Var             ( globaliseId )
 import Name            ( isBuiltInSyntax, isInternalName )
 import OccName         ( isTcOcc )
@@ -997,10 +997,12 @@ tcGhciStmts stmts
                -- then the type checker would instantiate x..z, and we wouldn't
                -- get their *polymorphic* values.  (And we'd get ambiguity errs
                -- if they were overloaded, since they aren't applied to anything.)
-           mk_return ids = nlHsApp (noLoc $ TyApp (nlHsVar ret_id) [ret_ty]) 
+           mk_return ids = nlHsApp (mkHsTyApp ret_id [ret_ty]) 
                                    (noLoc $ ExplicitList unitTy (map mk_item ids)) ;
-           mk_item id = nlHsApp (noLoc $ TyApp (nlHsVar unsafeCoerceId) [idType id, unitTy])
-                                (nlHsVar id) 
+           mk_item id = nlHsApp (noLoc $ unsafeCoerce)
+                                (nlHsVar id)
+            unsafeCoerce x = Cast x (mkUnsafeCoercion [idType id, unitTy]) 
         } ;
 
        -- OK, we're ready to typecheck the stmts
index 0b5e4fc..af75fe6 100644 (file)
@@ -132,33 +132,8 @@ initTc hsc_env hsc_src mod do_this
    
        -- OK, here's the business end!
        maybe_res <- initTcRnIf 'a' hsc_env gbl_env lcl_env $
-                    do {
-#if defined(GHCI) && defined(BREAKPOINT)
-                          unique <- newUnique ;
-                          let { var = mkInternalName unique (mkOccName tvName "a") noSrcLoc;
-                                tyvar = mkTyVar var liftedTypeKind;
-                                basicType extra = (FunTy intTy
-                                                   (FunTy (mkListTy unitTy)
-                                                    (FunTy stringTy
-                                                     (ForAllTy tyvar
-                                                      (extra
-                                                       (FunTy (TyVarTy tyvar)
-                                                        (TyVarTy tyvar)))))));
-                                breakpointJumpType
-                                    = mkGlobalId VanillaGlobal breakpointJumpName
-                                                 (basicType id) vanillaIdInfo;
-                                breakpointCondJumpType
-                                    = mkGlobalId VanillaGlobal breakpointCondJumpName
-                                                 (basicType (FunTy boolTy)) vanillaIdInfo;
-                                new_env = mkNameEnv [(breakpointJumpName
-                                                     , ATcId breakpointJumpType topLevel False)
-                                                     ,(breakpointCondJumpName
-                                                     , ATcId breakpointCondJumpType topLevel False)];
-                              };
-                          r <- tryM (updLclEnv (\gbl -> gbl{tcl_env=new_env}) do_this)
-#else
-                          r <- tryM do_this
-#endif
+                    addBreakpointBindings $
+                    do { r <- tryM do_this
                        ; case r of
                          Right res -> return (Just res)
                          Left _    -> return Nothing } ;
@@ -191,6 +166,32 @@ initTcPrintErrors env mod todo = do
   return res
 \end{code}
 
+\begin{code}
+addBreakpointBindings :: TcM a -> TcM a
+addBreakpointBindings thing_inside
+#if defined(GHCI) && defined(BREAKPOINT)
+  = do { unique <- newUnique
+        ; let { var = mkInternalName unique (mkOccName tvName "a") noSrcLoc;
+                tyvar = mkTyVar var liftedTypeKind;
+                basicType extra = (FunTy intTy
+                                   (FunTy (mkListTy unitTy)
+                                    (FunTy stringTy
+                                     (ForAllTy tyvar
+                                      (extra
+                                       (FunTy (TyVarTy tyvar)
+                                        (TyVarTy tyvar)))))));
+                breakpointJumpId
+                    = mkGlobalId VanillaGlobal breakpointJumpName
+                                 (basicType id) vanillaIdInfo;
+                breakpointCondJumpId
+                    = mkGlobalId VanillaGlobal breakpointCondJumpName
+                                 (basicType (FunTy boolTy)) vanillaIdInfo
+         }
+       ; extendIdEnv [breakpoingJumpId, breakpointCondJumpId] thing_inside}
+#else
+   = thing_inside
+#endif
+\end{code}
 
 %************************************************************************
 %*                                                                     *
index 3b12477..f66abdc 100644 (file)
@@ -21,7 +21,6 @@ module TcRnTypes(
 
        -- Typechecker types
        TcTyThing(..), pprTcTyThingCategory, 
-       GadtRefinement,
 
        -- Template Haskell
        ThStage(..), topStage, topSpliceStage,
@@ -44,7 +43,7 @@ module TcRnTypes(
 
 import HsSyn           ( PendingSplice, HsOverLit, LRuleDecl, LForeignDecl,
                          ArithSeqInfo, DictBinds, LHsBinds, LImportDecl, HsGroup,
-                          IE )
+                          ExprCoFn, IE )
 import HscTypes                ( FixityEnv,
                          HscEnv, TypeEnv, TyThing, 
                          GenAvailInfo(..), AvailInfo, HscSource(..),
@@ -324,7 +323,6 @@ data TcLclEnv               -- Changes as we move inside an expression
        tcl_lie   :: TcRef LIE          -- Place to accumulate type constraints
     }
 
-type GadtRefinement = TvSubst
 
 {- Note [Given Insts]
    ~~~~~~~~~~~~~~~~~~
@@ -419,9 +417,15 @@ escapeArrowScope
 data TcTyThing
   = AGlobal TyThing            -- Used only in the return type of a lookup
 
-  | ATcId   TcId               -- Ids defined in this module; may not be fully zonked
-           ThLevel 
-           Bool                -- True <=> apply the type refinement to me
+  | ATcId   {          -- Ids defined in this module; may not be fully zonked
+       tct_id :: TcId,         
+       tct_co :: Maybe ExprCoFn,       -- Nothing <=>  Do not apply a GADT type refinement
+                                       --              I am wobbly, or have no free
+                                       --              type variables
+                                       -- Just co <=>  Apply any type refinement to me,
+                                       --              and record it in the coercion
+       tct_type  :: TcType,    -- Type of (coercion applied to id)
+       tct_level :: ThLevel }
 
   | ATyVar  Name TcType                -- The type to which the lexically scoped type vaiable
                                -- is currently refined. We only need the Name
@@ -432,8 +436,9 @@ data TcTyThing
 
 instance Outputable TcTyThing where    -- Debugging only
    ppr (AGlobal g)      = ppr g
-   ppr (ATcId g tl rig) = text "Identifier" <> 
-                         ifPprDebug (brackets (ppr g <> comma <> ppr tl <+> ppr rig))
+   ppr elt@(ATcId {})   = text "Identifier" <> 
+                         ifPprDebug (brackets (ppr (tct_id elt) <> dcolon <> ppr (tct_type elt) <> comma
+                                <+> ppr (tct_level elt) <+> ppr (tct_co elt)))
    ppr (ATyVar tv _)    = text "Type variable" <+> quotes (ppr tv)
    ppr (AThing k)       = text "AThing" <+> ppr k
 
index 1998cd2..8f06270 100644 (file)
@@ -21,8 +21,9 @@ module TcSimplify (
 #include "HsVersions.h"
 
 import {-# SOURCE #-} TcUnify( unifyType )
-import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, emptyLHsBinds )
-import TcHsSyn         ( mkHsApp, mkHsTyApp, mkHsDictApp )
+import HsSyn           ( HsBind(..), HsExpr(..), LHsExpr, 
+                         ExprCoFn(..), (<.>), nlHsTyApp, emptyLHsBinds )
+import TcHsSyn         ( mkHsApp )
 
 import TcRnMonad
 import Inst            ( lookupInst, LookupInstResult(..),
@@ -31,7 +32,7 @@ import Inst           ( lookupInst, LookupInstResult(..),
                          isMethodFor, isMethod,
                          instToId, tyVarsOfInsts,  cloneDict,
                          ipNamesOfInsts, ipNamesOfInst, dictPred,
-                         fdPredsOfInst,
+                         fdPredsOfInst, mkInstCoFn,
                          newDictsAtLoc, tcInstClassOp,
                          getDictClassTys, isTyVarDict, instLoc,
                          zonkInst, tidyInsts, tidyMoreInsts,
@@ -1468,6 +1469,7 @@ extractResults avails wanteds
                   new_binds  = addBind binds w rhs
                   new_avails = addToFM avails w (LinRhss rhss)
 
+       -- get_root is just used for Linear
     get_root irreds frees (Given id _) w = returnM (irreds, frees, id)
     get_root irreds frees Irred               w = cloneDict w  `thenM` \ w' ->
                                           returnM (w':irreds, frees, instToId w')
@@ -1540,7 +1542,7 @@ split n split_id root_id wanted
                       returnM (L span (VarBind x (mk_app span split_id rhs)),
                                [mk_fs_app span fst_id ty x, mk_fs_app span snd_id ty x])
 
-mk_fs_app span id ty var = L span (HsVar id) `mkHsTyApp` [ty,ty] `mkHsApp` (L span (HsVar var))
+mk_fs_app span id ty var = nlHsTyApp id [ty,ty] `mkHsApp` (L span (HsVar var))
 
 mk_app span id rhs = L span (HsApp (L span (HsVar id)) rhs)
 
@@ -1922,7 +1924,8 @@ addSCs is_loop avails dict
       | is_given sc_dict          = return avails
       | otherwise                 = addSCs is_loop avails' sc_dict
       where
-       sc_sel_rhs = mkHsDictApp (mkHsTyApp (L (instSpan dict) (HsVar sc_sel)) tys) [instToId dict]
+       sc_sel_rhs = L (instSpan dict) (HsCoerce co_fn (HsVar sc_sel))
+       co_fn      = mkInstCoFn tys [dict]
        avails'    = addToFM avails sc_dict (Rhs sc_sel_rhs [dict])
 
     is_given :: Inst -> Bool
index 6ac66d6..d59b0f8 100644 (file)
@@ -567,9 +567,9 @@ reifyThing (AGlobal (ADataCon dc))
        ; fix <- reifyFixity name
        ; return (TH.DataConI (reifyName name) ty (reifyName (dataConTyCon dc)) fix) }
 
-reifyThing (ATcId id _ _
-  = do { ty1 <- zonkTcType (idType id) -- Make use of all the info we have, even
-                                       -- though it may be incomplete
+reifyThing (ATcId {tct_id = id, tct_ty = ty}
+  = do { ty1 <- zonkTcType ty  -- Make use of all the info we have, even
+                               -- though it may be incomplete
        ; ty2 <- reifyType ty1
        ; fix <- reifyFixity (idName id)
        ; return (TH.VarI (reifyName id) ty2 Nothing fix) }
index 090db01..3cf6145 100644 (file)
@@ -33,21 +33,20 @@ import TcHsType             ( kcHsTyVars, kcHsLiftedSigType, kcHsType,
 import TcMType         ( newKindVar, checkValidTheta, checkValidType, 
                          -- checkFreeness, 
                          UserTypeCtxt(..), SourceTyCtxt(..) ) 
-import TcType          ( TcKind, TcType, tyVarsOfType, mkPhiTy,
+import TcType          ( TcKind, TcType, Type, tyVarsOfType, mkPhiTy,
                          mkArrowKind, liftedTypeKind, mkTyVarTys, 
                          tcSplitSigmaTy, tcEqTypes, tcGetTyVar_maybe )
-import Type            ( splitTyConApp_maybe, 
+import Type            ( PredType(..), splitTyConApp_maybe, mkTyVarTy
                          -- pprParendType, pprThetaArrow
                        )
-import Kind            ( mkArrowKinds, splitKindFunTys )
 import Generics                ( validGenericMethodType, canDoGenerics )
 import Class           ( Class, className, classTyCon, DefMeth(..), classBigSig, classTyVars )
 import TyCon           ( TyCon, AlgTyConRhs( AbstractTyCon ),
                          tyConDataCons, mkForeignTyCon, isProductTyCon, isRecursiveTyCon,
                          tyConStupidTheta, synTyConRhs, isSynTyCon, tyConName )
-import DataCon         ( DataCon, dataConWrapId, dataConName, 
-                         dataConFieldLabels, dataConTyCon,
-                         dataConTyVars, dataConFieldType, dataConResTys )
+import DataCon         ( DataCon, dataConUserType, dataConName, 
+                         dataConFieldLabels, dataConTyCon, dataConAllTyVars,
+                         dataConFieldType, dataConResTys )
 import Var             ( TyVar, idType, idName )
 import VarSet          ( elemVarSet, mkVarSet )
 import Name            ( Name, getSrcLoc )
@@ -58,7 +57,7 @@ import Unify          ( tcMatchTys, tcMatchTyX )
 import Util            ( zipLazy, isSingleton, notNull, sortLe )
 import List            ( partition )
 import SrcLoc          ( Located(..), unLoc, getLoc, srcLocSpan )
-import ListSetOps      ( equivClasses )
+import ListSetOps      ( equivClasses, minusList )
 import List            ( delete )
 import Digraph         ( SCC(..) )
 import DynFlags                ( DynFlag( Opt_GlasgowExts, Opt_Generics, 
@@ -427,8 +426,11 @@ tcTyClDecl1 calc_isrec
        -- Check that we don't use GADT syntax in H98 world
   ; checkTc (gla_exts || h98_syntax) (badGadtDecl tc_name)
 
+       -- Check that the stupid theta is empty for a GADT-style declaration
+  ; checkTc (null stupid_theta || h98_syntax) (badStupidTheta tc_name)
+
        -- Check that there's at least one condecl,
-       -- or else we're reading an interface file, or -fglasgow-exts
+       -- or else we're reading an hs-boot file, or -fglasgow-exts
   ; checkTc (not (null cons) || gla_exts || is_boot)
            (emptyConDeclsErr tc_name)
     
@@ -440,16 +442,16 @@ tcTyClDecl1 calc_isrec
        { data_cons <- mappM (addLocM (tcConDecl unbox_strict new_or_data 
                                                 tycon final_tvs)) 
                             cons
-       ; let tc_rhs 
-               | null cons && is_boot  -- In a hs-boot file, empty cons means
-               = AbstractTyCon         -- "don't know"; hence Abstract
-               | otherwise
-               = case new_or_data of
-                       DataType -> mkDataTyConRhs data_cons
-                       NewType  -> ASSERT( isSingleton data_cons )
-                                   mkNewTyConRhs tycon (head data_cons)
+       ; tc_rhs <-
+           if null cons && is_boot     -- In a hs-boot file, empty cons means
+           then return AbstractTyCon   -- "don't know"; hence Abstract
+           else case new_or_data of
+                  DataType -> return (mkDataTyConRhs data_cons)
+                  NewType  -> 
+                       ASSERT( isSingleton data_cons )
+                       mkNewTyConRhs tc_name tycon (head data_cons)
        ; buildAlgTyCon tc_name final_tvs stupid_theta tc_rhs is_rec
-                       (want_generic && canDoGenerics data_cons)
+                       (want_generic && canDoGenerics data_cons) h98_syntax
        })
   ; return (ATyCon tycon)
   }
@@ -498,10 +500,12 @@ tcConDecl unbox_strict NewType tycon tc_tvs       -- Newtypes
   = do { let tc_datacon field_lbls arg_ty
                = do { arg_ty' <- tcHsKindedType arg_ty -- No bang on newtype
                     ; buildDataCon (unLoc name) False {- Prefix -} 
-                                   True {- Vanilla -} [NotMarkedStrict]
+                                   [NotMarkedStrict]
                                    (map unLoc field_lbls)
-                                   tc_tvs [] [arg_ty']
-                                   tycon (mkTyVarTys tc_tvs) }
+                                   tc_tvs []  -- No existentials
+                                   [] []      -- No equalities, predicates
+                                   [arg_ty']
+                                   tycon }
 
                -- Check that a newtype has no existential stuff
        ; checkTc (null ex_tvs && null (unLoc ex_ctxt)) (newtypeExError name)
@@ -517,27 +521,16 @@ tcConDecl unbox_strict DataType tycon tc_tvs      -- Data types
          (ConDecl name _ tvs ctxt details res_ty)
   = tcTyVarBndrs tvs           $ \ tvs' -> do 
     { ctxt' <- tcHsKindedContext ctxt
-    ; (data_tc, res_ty_args) <- tcResultType tycon tc_tvs res_ty
+    ; (univ_tvs, ex_tvs, eq_preds, data_tc) <- tcResultType tycon tc_tvs tvs' res_ty
     ; let 
-       con_tvs = case res_ty of
-                   ResTyH98    -> tc_tvs ++ tvs'
-                   ResTyGADT _ -> tryVanilla tvs' res_ty_args
-
-       -- Vanilla iff result type matches the quantified vars exactly,
-       -- and there is no existential context
-       -- Must check the context too because of implicit params; e.g.
-       --      data T = (?x::Int) => MkT Int
-       is_vanilla = res_ty_args `tcEqTypes` mkTyVarTys con_tvs
-                    && null (unLoc ctxt)
-
        tc_datacon is_infix field_lbls btys
          = do { let bangs = map getBangStrictness btys
               ; arg_tys <- mappM tcHsBangType btys
-              ; buildDataCon (unLoc name) is_infix is_vanilla
+              ; buildDataCon (unLoc name) is_infix
                    (argStrictness unbox_strict tycon bangs arg_tys)
                    (map unLoc field_lbls)
-                   con_tvs ctxt' arg_tys
-                   data_tc res_ty_args }
+                   univ_tvs ex_tvs eq_preds ctxt' arg_tys
+                   data_tc }
                -- NB:  we put data_tc, the type constructor gotten from the constructor 
                --      type signature into the data constructor; that way 
                --      checkValidDataCon can complain if it's wrong.
@@ -551,19 +544,48 @@ tcConDecl unbox_strict DataType tycon tc_tvs      -- Data types
                               
     }
 
-tcResultType :: TyCon -> [TyVar] -> ResType Name -> TcM (TyCon, [TcType])
-tcResultType tycon tvs ResTyH98           = return (tycon, mkTyVarTys tvs)
-tcResultType _     _   (ResTyGADT res_ty) = tcLHsConResTy res_ty
-
-tryVanilla :: [TyVar] -> [TcType] -> [TyVar]
--- (tryVanilla tvs tys) returns a permutation of tvs.
--- It tries to re-order the tvs so that it exactly 
--- matches the [Type], if that is possible
-tryVanilla tvs (ty:tys) | Just tv <- tcGetTyVar_maybe ty       -- The type is a tyvar
-                       , tv `elem` tvs                         -- That tyvar is in the list
-                       = tv : tryVanilla (delete tv tvs) tys
-tryVanilla tvs tys = tvs       -- Fall through case
-
+tcResultType :: TyCon
+            -> [TyVar]         -- data T a b c = ...
+            -> [TyVar]         -- where MkT :: forall a b c. ...
+            -> ResType Name
+            -> TcM ([TyVar],           -- Universal
+                    [TyVar],           -- Existential
+                    [(TyVar,Type)],    -- Equality predicates
+                    TyCon)             -- TyCon given in the ResTy
+       -- We don't check that the TyCon given in the ResTy is
+       -- the same as the parent tycon, becuase we are in the middle
+       -- of a recursive knot; so it's postponed until checkValidDataCon
+
+tcResultType decl_tycon tc_tvs dc_tvs ResTyH98
+  = return (tc_tvs, dc_tvs, [], decl_tycon)
+       -- In H98 syntax the dc_tvs are the existential ones
+       --      data T a b c = forall d e. MkT ...
+       -- The {a,b,c} are tc_tvs, and {d,e} are dc_tvs
+
+tcResultType _ tc_tvs dc_tvs (ResTyGADT res_ty)
+       -- E.g.  data T a b c where
+       --         MkT :: forall x y z. T (x,y) z z
+       -- Then we generate
+       --      ([a,z,c], [x,y], [a:=:(x,y), c:=:z], T)
+
+  = do { (dc_tycon, res_tys) <- tcLHsConResTy res_ty
+               -- NB: tc_tvs and dc_tvs are distinct
+       ; let univ_tvs = choose_univs [] tc_tvs res_tys
+               -- Each univ_tv is either a dc_tv or a tc_tv
+             ex_tvs = dc_tvs `minusList` univ_tvs
+             eq_spec = [ (tv, ty) | (tv,ty) <- univ_tvs `zip` res_tys, 
+                                     tv `elem` tc_tvs]
+       ; return (univ_tvs, ex_tvs, eq_spec, dc_tycon) }
+  where
+       -- choose_univs uses the res_ty itself if it's a type variable
+       -- and hasn't already been used; otherwise it uses one of the tc_tvs
+    choose_univs used tc_tvs []
+       = ASSERT( null tc_tvs ) []
+    choose_univs used (tc_tv:tc_tvs) (res_ty:res_tys) 
+       | Just tv <- tcGetTyVar_maybe res_ty, not (tv `elem` used)
+       = tv    : choose_univs (tv:used) tc_tvs res_tys
+       | otherwise
+       = tc_tv : choose_univs used tc_tvs res_tys
 
 -------------------
 argStrictness :: Bool          -- True <=> -funbox-strict_fields
@@ -634,7 +656,7 @@ checkValidTyCl decl
 -- of the constructor.
 
 checkValidTyCon :: TyCon -> TcM ()
-checkValidTyCon tc
+checkValidTyCon tc 
   | isSynTyCon tc 
   = checkValidType syn_ctxt syn_rhs
   | otherwise
@@ -658,14 +680,20 @@ checkValidTyCon tc
     get_fields con = dataConFieldLabels con `zip` repeat con
        -- dataConFieldLabels may return the empty list, which is fine
 
-    -- Note: The complicated checkOne logic below is there to accomodate
-    --       for different return types.  Add res_ty to the mix,
-    --       comparing them in two steps, all for good error messages.
-    --       Plan: Use Unify.tcMatchTys to compare the first candidate's
-    --             result type against other candidates' types (check bothways).
-    --             If they magically agrees, take the substitution and
-    --             apply them to the latter ones, and see if they match perfectly.
-    -- check_fields fields@((first_field_label, field_ty) : other_fields)
+    -- See Note [GADT record selectors] in MkId.lhs
+    -- We must check (a) that the named field has the same 
+    --                   type in each constructor
+    --               (b) that those constructors have the same result type
+    --
+    -- However, the constructors may have differently named type variable
+    -- and (worse) we don't know how the correspond to each other.  E.g.
+    --     C1 :: forall a b. { f :: a, g :: b } -> T a b
+    --     C2 :: forall d c. { f :: c, g :: c } -> T c d
+    -- 
+    -- So what we do is to ust Unify.tcMatchTys to compare the first candidate's
+    -- result type against other candidates' types BOTH WAYS ROUND.
+    -- If they magically agrees, take the substitution and
+    -- apply them to the latter ones, and see if they match perfectly.
     check_fields fields@((label, con1) : other_fields)
        -- These fields all have the same name, but are from
        -- different constructors in the data type
@@ -674,7 +702,7 @@ checkValidTyCon tc
                -- NB: this check assumes that all the constructors of a given
                -- data type use the same type variables
         where
-        tvs1 = mkVarSet (dataConTyVars con1)
+        tvs1 = mkVarSet (dataConAllTyVars con1)
         res1 = dataConResTys con1
         fty1 = dataConFieldType con1 label
 
@@ -682,7 +710,7 @@ checkValidTyCon tc
            = do { checkFieldCompat label con1 con2 tvs1 res1 res2 fty1 fty2
                 ; checkFieldCompat label con2 con1 tvs2 res2 res1 fty2 fty1 }
            where        
-                tvs2 = mkVarSet (dataConTyVars con2)
+                tvs2 = mkVarSet (dataConAllTyVars con2)
                res2 = dataConResTys con2 
                 fty2 = dataConFieldType con2 label
 
@@ -699,18 +727,9 @@ checkValidDataCon tc con
   = setSrcSpan (srcLocSpan (getSrcLoc con))    $
     addErrCtxt (dataConCtxt con)               $ 
     do { checkTc (dataConTyCon con == tc) (badDataConTyCon con)
-       ; checkValidType ctxt (idType (dataConWrapId con)) }
-
-               -- This checks the argument types and
-               -- ambiguity of the existential context (if any)
-               -- 
-               -- Note [Sept 04] Now that tvs is all the tvs, this
-               -- test doesn't actually check anything
---     ; checkFreeness tvs ex_theta }
+       ; checkValidType ctxt (dataConUserType con) }
   where
     ctxt = ConArgCtxt (dataConName con) 
---    (tvs, ex_theta, _, _, _) = dataConSig con
-
 
 -------------------------------
 checkValidClass :: Class -> TcM ()
@@ -840,6 +859,9 @@ badGadtDecl tc_name
   = vcat [ ptext SLIT("Illegal generalised algebraic data declaration for") <+> quotes (ppr tc_name)
         , nest 2 (parens $ ptext SLIT("Use -fglasgow-exts to allow GADTs")) ]
 
+badStupidTheta tc_name
+  = ptext SLIT("A data type declared in GADT style cannot have a context:") <+> quotes (ppr tc_name)
+
 newtypeConError tycon n
   = sep [ptext SLIT("A newtype must have exactly one constructor,"),
         nest 2 $ ptext SLIT("but") <+> quotes (ppr tycon) <+> ptext SLIT("has") <+> speakN n ]
index a21f0fb..06eb0dc 100644 (file)
@@ -42,7 +42,7 @@ module TcType (
   tcSplitForAllTys, tcSplitPhiTy, 
   tcSplitFunTy_maybe, tcSplitFunTys, tcFunArgTy, tcFunResultTy, tcSplitFunTysN,
   tcSplitTyConApp, tcSplitTyConApp_maybe, tcTyConAppTyCon, tcTyConAppArgs,
-  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, 
+  tcSplitAppTy_maybe, tcSplitAppTy, tcSplitAppTys, repSplitAppTy_maybe,
   tcValidInstHeadTy, tcGetTyVar_maybe, tcGetTyVar,
   tcSplitSigmaTy, tcMultiSplitSigmaTy, 
 
@@ -50,6 +50,7 @@ module TcType (
   -- Predicates. 
   -- Again, newtypes are opaque
   tcEqType, tcEqTypes, tcEqPred, tcCmpType, tcCmpTypes, tcCmpPred, tcEqTypeX,
+  eqKind, 
   isSigmaTy, isOverloadedTy, isRigidTy, isBoxyTy,
   isDoubleTy, isFloatTy, isIntTy, isStringTy,
   isIntegerTy, isBoolTy, isUnitTy,
@@ -64,7 +65,7 @@ module TcType (
   ---------------------------------
   -- Predicate types  
   getClassPredTys_maybe, getClassPredTys, 
-  isClassPred, isTyVarClassPred, 
+  isClassPred, isTyVarClassPred, isEqPred, 
   mkDictTy, tcSplitPredTy_maybe, 
   isPredTy, isDictTy, tcSplitDFunTy, tcSplitDFunHead, predTyUnique, 
   mkClassPred, isInheritablePred, isLinearPred, isIPPred, mkPredName, 
@@ -90,8 +91,9 @@ module TcType (
   Kind,        -- Stuff to do with kinds is insensitive to pre/post Tc
   unliftedTypeKind, liftedTypeKind, unboxedTypeKind, argTypeKind,
   openTypeKind, mkArrowKind, mkArrowKinds, 
-  isLiftedTypeKind, isUnliftedTypeKind, isOpenTypeKind, 
-  isArgTypeKind, isSubKind, defaultKind, 
+  isLiftedTypeKind, isUnliftedTypeKind, isSubOpenTypeKind, 
+  isSubArgTypeKind, isSubKind, defaultKind,
+  kindVarRef, mkKindVar,  
 
   Type, PredType(..), ThetaType, 
   mkForAllTy, mkForAllTys, 
@@ -101,7 +103,7 @@ module TcType (
 
   -- Type substitutions
   TvSubst(..),         -- Representation visible to a few friends
-  TvSubstEnv, emptyTvSubst,
+  TvSubstEnv, emptyTvSubst, substEqSpec,
   mkOpenTvSubst, zipOpenTvSubst, zipTopTvSubst, mkTopTvSubst, notElemTvSubst,
   getTvSubstEnv, setTvSubstEnv, getTvInScope, extendTvInScope, lookupTyVar,
   extendTvSubst, extendTvSubstList, isInScope, mkTvSubst, zipTyEnv,
@@ -127,16 +129,18 @@ module TcType (
 #include "HsVersions.h"
 
 -- friends:
-import TypeRep         ( Type(..), funTyCon )  -- friend
+import TypeRep         ( Type(..), funTyCon, Kind )  -- friend
 
 import Type            (       -- Re-exports
                          tyVarsOfType, tyVarsOfTypes, tyVarsOfPred,
-                         tyVarsOfTheta, Kind, PredType(..),
-                         ThetaType, unliftedTypeKind, unboxedTypeKind, argTypeKind,
+                         tyVarsOfTheta, Kind, PredType(..), KindVar,
+                         ThetaType, isUnliftedTypeKind, unliftedTypeKind, 
+-- ???                   unboxedTypeKind,
+                         argTypeKind,
                          liftedTypeKind, openTypeKind, mkArrowKind,
-                         isLiftedTypeKind, isUnliftedTypeKind, 
+                         tySuperKind, isLiftedTypeKind,
                          mkArrowKinds, mkForAllTy, mkForAllTys,
-                         defaultKind, isArgTypeKind, isOpenTypeKind,
+                         defaultKind, isSubArgTypeKind, isSubOpenTypeKind,
                          mkFunTy, mkFunTys, zipFunTys, 
                          mkTyConApp, mkAppTy,
                          mkAppTys, applyTy, applyTys,
@@ -151,7 +155,7 @@ import Type         (       -- Re-exports
                          isSubKind, tcView,
 
                          tcEqType, tcEqTypes, tcCmpType, tcCmpTypes, 
-                         tcEqPred, tcCmpPred, tcEqTypeX, 
+                         tcEqPred, tcCmpPred, tcEqTypeX, eqKind,
 
                          TvSubst(..),
                          TvSubstEnv, emptyTvSubst, mkTvSubst, zipTyEnv,
@@ -161,7 +165,7 @@ import Type         (       -- Re-exports
                          substTy, substTys, substTyWith, substTheta, 
                          substTyVar, substTyVarBndr, substPred, lookupTyVar,
 
-                         typeKind, repType, coreView,
+                         typeKind, repType, coreView, repSplitAppTy_maybe,
                          pprKind, pprParendKind,
                          pprType, pprParendType, pprTyThingCategory,
                          pprPred, pprTheta, pprThetaArrow, pprClassPred
@@ -176,10 +180,10 @@ import VarSet
 
 -- others:
 import DynFlags                ( DynFlags, DynFlag( Opt_GlasgowExts ), dopt )
-import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc )
+import Name            ( Name, NamedThing(..), mkInternalName, getSrcLoc, mkSystemName )
 import NameSet
 import VarEnv          ( TidyEnv )
-import OccName         ( OccName, mkDictOcc )
+import OccName         ( OccName, mkDictOcc, mkOccName, tvName )
 import PrelNames       -- Lots (e.g. in isFFIArgumentTy)
 import TysWiredIn      ( unitTyCon, charTyCon, listTyCon )
 import BasicTypes      ( IPName(..), Arity, ipNameName )
@@ -385,6 +389,31 @@ data UserTypeCtxt
 -- will become type T = forall a. a->a
 --
 -- With gla-exts that's right, but for H98 we should complain. 
+
+---------------------------------
+-- Kind variables:
+
+mkKindName :: Unique -> Name
+mkKindName unique = mkSystemName unique kind_var_occ
+
+kindVarRef :: KindVar -> IORef MetaDetails
+kindVarRef tc = 
+  case tcTyVarDetails tc of
+    MetaTv TauTv ref -> ref
+    other            -> pprPanic "kindVarRef" (ppr tc)
+
+mkKindVar :: Unique -> IORef MetaDetails -> KindVar
+mkKindVar u r 
+  = mkTcTyVar (mkKindName u)
+              tySuperKind  -- not sure this is right,
+                            -- do we need kind vars for
+                            -- coercions?
+              (MetaTv TauTv r)
+
+kind_var_occ :: OccName        -- Just one for all KindVars
+                       -- They may be jiggled by tidying
+kind_var_occ = mkOccName tvName "k"
+\end{code}
 \end{code}
 
 %************************************************************************
@@ -708,13 +737,9 @@ tcFunResultTy ty = snd (tcSplitFunTy ty)
 -----------------------
 tcSplitAppTy_maybe :: Type -> Maybe (Type, Type)
 tcSplitAppTy_maybe ty | Just ty' <- tcView ty = tcSplitAppTy_maybe ty'
-tcSplitAppTy_maybe (FunTy ty1 ty2)   = Just (TyConApp funTyCon [ty1], ty2)
-tcSplitAppTy_maybe (AppTy ty1 ty2)   = Just (ty1, ty2)
-tcSplitAppTy_maybe (TyConApp tc tys) = case snocView tys of
-                                       Just (tys', ty') -> Just (TyConApp tc tys', ty')
-                                       Nothing          -> Nothing
-tcSplitAppTy_maybe other            = Nothing
+tcSplitAppTy_maybe ty = repSplitAppTy_maybe ty
 
+tcSplitAppTy :: Type -> (Type, Type)
 tcSplitAppTy ty = case tcSplitAppTy_maybe ty of
                    Just stuff -> stuff
                    Nothing    -> pprPanic "tcSplitAppTy" (pprType ty)
@@ -820,6 +845,10 @@ getClassPredTys :: PredType -> (Class, [Type])
 getClassPredTys (ClassP clas tys) = (clas, tys)
 getClassPredTys other = panic "getClassPredTys"
 
+isEqPred :: PredType -> Bool
+isEqPred (EqPred {}) = True
+isEqPred _          = False
+
 mkDictTy :: Class -> [Type] -> Type
 mkDictTy clas tys = mkPredTy (ClassP clas tys)
 
@@ -853,6 +882,13 @@ isLinearPred (IParam (Linear n) _) = True
 isLinearPred other                = False
 \end{code}
 
+--------------------- Equality predicates ---------------------------------
+\begin{code}
+substEqSpec :: TvSubst -> [(TyVar,Type)] -> [(TcType,TcType)]
+substEqSpec subst eq_spec = [ (substTyVar subst tv, substTy subst ty)
+                           | (tv,ty) <- eq_spec]
+\end{code}
+
 --------------------- The stupid theta (sigh) ---------------------------------
 
 \begin{code}
@@ -937,7 +973,8 @@ deNoteType ty = ty
 
 \begin{code}
 tcTyVarsOfType :: Type -> TcTyVarSet
--- Just the tc type variables free in the type
+-- Just the *TcTyVars* free in the type
+-- (Types.tyVarsOfTypes finds all free TyVars)
 tcTyVarsOfType (TyVarTy tv)        = if isTcTyVar tv then unitVarSet tv
                                                      else emptyVarSet
 tcTyVarsOfType (TyConApp tycon tys) = tcTyVarsOfTypes tys
index 191badd..15c2367 100644 (file)
@@ -2,6 +2,8 @@
 module TcType where
 import Outputable( SDoc )
 
+data MetaDetails
+
 data TcTyVarDetails 
 pprTcTyVarDetails :: TcTyVarDetails -> SDoc
 \end{code}
index 5b02241..1295ab3 100644 (file)
@@ -54,13 +54,14 @@ import TcType               ( TcKind, TcType, TcTyVar, BoxyTyVar, TcTauType,
                          TvSubst, mkTvSubst, zipTyEnv, zipOpenTvSubst, emptyTvSubst, 
                          substTy, substTheta, 
                          lookupTyVar, extendTvSubst )
-import Kind            ( Kind(..), SimpleKind, KindVar, isArgTypeKind,
+import Type            ( Kind, SimpleKind, KindVar, 
                          openTypeKind, liftedTypeKind, unliftedTypeKind, 
                          mkArrowKind, defaultKind,
-                         isOpenTypeKind, argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
-                         isSubKind, pprKind, splitKindFunTys )
+                         argTypeKind, isLiftedTypeKind, isUnliftedTypeKind,
+                         isSubKind, pprKind, splitKindFunTys, isSubKindCon,
+                          isOpenTypeKind, isArgTypeKind )
 import TysPrim         ( alphaTy, betaTy )
-import Inst            ( newDicts, instToId )
+import Inst            ( newDicts, instToId, mkInstCoFn )
 import TyCon           ( TyCon, tyConArity, tyConTyVars, isSynTyCon )
 import TysWiredIn      ( listTyCon )
 import Id              ( Id, mkSysLocal )
@@ -601,11 +602,13 @@ tcSubExp actual_ty expected_ty
     -- Adding the error context here leads to some very confusing error
     -- messages, such as "can't match foarall a. a->a with forall a. a->a"
     -- So instead I'm adding it when moving from tc_sub to u_tys
+    traceTc (text "tcSubExp" <+> ppr actual_ty <+> ppr expected_ty) >>
     tc_sub Nothing actual_ty actual_ty False expected_ty expected_ty
 
 tcFunResTy :: Name -> BoxySigmaType -> BoxySigmaType -> TcM ExprCoFn   -- Locally used only
 tcFunResTy fun actual_ty expected_ty
-  = tc_sub (Just fun) actual_ty actual_ty False expected_ty expected_ty
+  = traceTc (text "tcFunResTy" <+> ppr actual_ty <+> ppr expected_ty) >>
+    tc_sub (Just fun) actual_ty actual_ty False expected_ty expected_ty
                   
 -----------------
 tc_sub :: Maybe Name           -- Just fun => we're looking at a function result type
@@ -700,8 +703,7 @@ tc_sub1 mb_fun act_sty actual_ty exp_ib exp_sty expected_ty
                -- Deal with the dictionaries
        ; dicts <- newDicts InstSigOrigin (substTheta subst' theta)
        ; extendLIEs dicts
-       ; let inst_fn = CoApps (CoTyApps CoHole inst_tys) 
-                              (map instToId dicts)
+       ; let inst_fn = mkInstCoFn inst_tys dicts
        ; return (co_fn <.> inst_fn) }
 
 -----------------------------------
@@ -746,7 +748,7 @@ wrapFunResCoercion arg_tys co_fn_res
   | otherwise         
   = do { us <- newUniqueSupply
        ; let arg_ids = zipWith (mkSysLocal FSLIT("sub")) (uniqsFromSupply us) arg_tys
-       ; return (CoLams arg_ids (co_fn_res <.> (CoApps CoHole arg_ids))) }
+       ; return (CoLams arg_ids <.> co_fn_res <.> CoApps arg_ids) }
 \end{code}
 
 
@@ -807,11 +809,9 @@ tcGen expected_ty extra_tvs thing_inside   -- We expect expected_ty to be a forall
        ; traceTc (text "tcGen:done")
 
        ; let
-           -- This HsLet binds any Insts which came out of the simplification.
-           -- It's a bit out of place here, but using AbsBind involves inventing
-           -- a couple of new names which seems worse.
-               dict_ids   = map instToId dicts
-               co_fn = CoTyLams forall_tvs $ CoLams dict_ids $ CoLet inst_binds CoHole 
+           -- The CoLet binds any Insts which came out of the simplification.
+               dict_ids = map instToId dicts
+               co_fn = CoTyLams forall_tvs <.> CoLams dict_ids <.> CoLet inst_binds
        ; returnM (co_fn, result) }
   where
     free_tvs = tyVarsOfType expected_ty `unionVarSet` extra_tvs
@@ -921,8 +921,10 @@ uTysOuter, uTys
      :: InBox -> TcType        -- ty1 is the *expected* type
      -> InBox -> TcType        -- ty2 is the *actual* type
      -> TcM ()
-uTysOuter nb1 ty1 nb2 ty2 = u_tys True nb1 ty1 ty1 nb2 ty2 ty2
-uTys      nb1 ty1 nb2 ty2 = u_tys False nb1 ty1 ty1 nb2 ty2 ty2
+uTysOuter nb1 ty1 nb2 ty2 = do { traceTc (text "uTysOuter" <+> ppr ty1 <+> ppr ty2)
+                              ; u_tys True nb1 ty1 ty1 nb2 ty2 ty2 }
+uTys      nb1 ty1 nb2 ty2 = do { traceTc (text "uTys" <+> ppr ty1 <+> ppr ty2)
+                              ; u_tys False nb1 ty1 ty1 nb2 ty2 ty2 }
 
 
 --------------
@@ -1101,7 +1103,7 @@ uVar outer swapped tv1 nb2 ps_ty2 ty2
                        | otherwise = brackets (equals <+> ppr ty2)
        ; traceTc (text "uVar" <+> ppr swapped <+> 
                        sep [ppr tv1 <+> dcolon <+> ppr (tyVarKind tv1 ),
-                               nest 2 (ptext SLIT(" :=: ")),
+                               nest 2 (ptext SLIT(" <-> ")),
                             ppr ps_ty2 <+> dcolon <+> ppr (typeKind ty2) <+> expansion])
        ; details <- lookupTcTyVar tv1
        ; case details of
@@ -1581,20 +1583,15 @@ Unifying kinds is much, much simpler than unifying types.
 unifyKind :: TcKind                -- Expected
          -> TcKind                 -- Actual
          -> TcM ()
-unifyKind LiftedTypeKind   LiftedTypeKind   = returnM ()
-unifyKind UnliftedTypeKind UnliftedTypeKind = returnM ()
+unifyKind (TyConApp kc1 []) (TyConApp kc2 []) 
+  | isSubKindCon kc2 kc1 = returnM ()
 
-unifyKind OpenTypeKind k2 | isOpenTypeKind k2 = returnM ()
-unifyKind ArgTypeKind  k2 | isArgTypeKind k2    = returnM ()
-  -- Respect sub-kinding
-
-unifyKind (FunKind a1 r1) (FunKind a2 r2)
- = do { unifyKind a2 a1; unifyKind r1 r2 }
+unifyKind (FunTy a1 r1) (FunTy a2 r2)
+  = do { unifyKind a2 a1; unifyKind r1 r2 }
                -- Notice the flip in the argument,
                -- so that the sub-kinding works right
-
-unifyKind (KindVar kv1) k2 = uKVar False kv1 k2
-unifyKind k1 (KindVar kv2) = uKVar True kv2 k1
+unifyKind (TyVarTy kv1) k2 = uKVar False kv1 k2
+unifyKind k1 (TyVarTy kv2) = uKVar True kv2 k1
 unifyKind k1 k2 = unifyKindMisMatch k1 k2
 
 unifyKinds :: [TcKind] -> [TcKind] -> TcM ()
@@ -1608,19 +1605,19 @@ uKVar :: Bool -> KindVar -> TcKind -> TcM ()
 uKVar swapped kv1 k2
   = do         { mb_k1 <- readKindVar kv1
        ; case mb_k1 of
-           Nothing -> uUnboundKVar swapped kv1 k2
-           Just k1 | swapped   -> unifyKind k2 k1
-                   | otherwise -> unifyKind k1 k2 }
+           Flexi -> uUnboundKVar swapped kv1 k2
+           Indirect k1 | swapped   -> unifyKind k2 k1
+                       | otherwise -> unifyKind k1 k2 }
 
 ----------------
 uUnboundKVar :: Bool -> KindVar -> TcKind -> TcM ()
-uUnboundKVar swapped kv1 k2@(KindVar kv2)
+uUnboundKVar swapped kv1 k2@(TyVarTy kv2)
   | kv1 == kv2 = returnM ()
   | otherwise  -- Distinct kind variables
   = do { mb_k2 <- readKindVar kv2
        ; case mb_k2 of
-           Just k2 -> uUnboundKVar swapped kv1 k2
-           Nothing -> writeKindVar kv1 k2 }
+           Indirect k2 -> uUnboundKVar swapped kv1 k2
+           Flexi       -> writeKindVar kv1 k2 }
 
 uUnboundKVar swapped kv1 non_var_k2
   = do { k2' <- zonkTcKind non_var_k2
@@ -1637,9 +1634,9 @@ uUnboundKVar swapped kv1 non_var_k2
 kindOccurCheck kv1 k2  -- k2 is zonked
   = checkTc (not_in k2) (kindOccurCheckErr kv1 k2)
   where
-    not_in (KindVar kv2)   = kv1 /= kv2
-    not_in (FunKind a2 r2) = not_in a2 && not_in r2
-    not_in other          = True
+    not_in (TyVarTy kv2)   = kv1 /= kv2
+    not_in (FunTy a2 r2) = not_in a2 && not_in r2
+    not_in other         = True
 
 kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 -- (kindSimpleKind True k) returns a simple kind sk such that sk <: k
@@ -1649,14 +1646,16 @@ kindSimpleKind :: Bool -> Kind -> TcM SimpleKind
 kindSimpleKind orig_swapped orig_kind
   = go orig_swapped orig_kind
   where
-    go sw (FunKind k1 k2) = do { k1' <- go (not sw) k1
-                              ; k2' <- go sw k2
-                              ; return (FunKind k1' k2') }
-    go True OpenTypeKind = return liftedTypeKind
-    go True ArgTypeKind  = return liftedTypeKind
-    go sw LiftedTypeKind  = return liftedTypeKind
-    go sw UnliftedTypeKind = return unliftedTypeKind
-    go sw k@(KindVar _)          = return k    -- KindVars are always simple
+    go sw (FunTy k1 k2) = do { k1' <- go (not sw) k1
+                            ; k2' <- go sw k2
+                            ; return (mkArrowKind k1' k2') }
+    go True k
+     | isOpenTypeKind k = return liftedTypeKind
+     | isArgTypeKind k  = return liftedTypeKind
+    go sw k
+     | isLiftedTypeKind k   = return liftedTypeKind
+     | isUnliftedTypeKind k = return unliftedTypeKind
+    go sw k@(TyVarTy _)          = return k    -- KindVars are always simple
     go swapped kind = failWithTc (ptext SLIT("Unexpected kind unification failure:")
                                  <+> ppr orig_swapped <+> ppr orig_kind)
        -- I think this can't actually happen
@@ -1685,17 +1684,18 @@ unifyKindMisMatch ty1 ty2
 unifyFunKind :: TcKind -> TcM (Maybe (TcKind, TcKind))
 -- Like unifyFunTy, but does not fail; instead just returns Nothing
 
-unifyFunKind (KindVar kvar)
-  = readKindVar kvar   `thenM` \ maybe_kind ->
+unifyFunKind (TyVarTy kvar)
+  = readKindVar kvar `thenM` \ maybe_kind ->
     case maybe_kind of
-       Just fun_kind -> unifyFunKind fun_kind
-       Nothing       -> do { arg_kind <- newKindVar
-                           ; res_kind <- newKindVar
-                           ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
-                           ; returnM (Just (arg_kind,res_kind)) }
+      Indirect fun_kind -> unifyFunKind fun_kind
+      Flexi             -> 
+          do { arg_kind <- newKindVar
+             ; res_kind <- newKindVar
+             ; writeKindVar kvar (mkArrowKind arg_kind res_kind)
+             ; returnM (Just (arg_kind,res_kind)) }
     
-unifyFunKind (FunKind arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
-unifyFunKind other                      = returnM Nothing
+unifyFunKind (FunTy arg_kind res_kind) = returnM (Just (arg_kind,res_kind))
+unifyFunKind other                    = returnM Nothing
 \end{code}
 
 %************************************************************************