This BIG PATCH contains most of the work for the New Coercion Representation
[ghc-hetmet.git] / compiler / typecheck / TcPat.lhs
index 1e391de..2501225 100644 (file)
@@ -32,7 +32,6 @@ import Coercion
 import StaticFlags
 import TyCon
 import DataCon
-import VarSet  ( emptyVarSet )
 import PrelNames
 import BasicTypes hiding (SuccessFlag(..))
 import DynFlags
@@ -59,14 +58,13 @@ tcLetPat :: TcSigFun -> LetBndrSpec
 tcLetPat sig_fn no_gen pat pat_ty thing_inside
   = tc_lpat pat pat_ty penv thing_inside 
   where
-    penv = PE { pe_res_tvs = emptyVarSet, pe_lazy = True
+    penv = PE { pe_lazy = True
               , pe_ctxt = LetPat sig_fn no_gen }
 
 -----------------
 tcPats :: HsMatchContext Name
        -> [LPat Name]           -- Patterns,
        -> [TcSigmaType]                 --   and their types
-       -> TcRhoType             -- Result type,
        -> TcM a                  --   and the checker for the body
        -> TcM ([LPat TcId], a)
 
@@ -81,39 +79,27 @@ tcPats :: HsMatchContext Name
 --   3. Check the body
 --   4. Check that no existentials escape
 
-tcPats ctxt pats pat_tys res_ty thing_inside
+tcPats ctxt pats pat_tys thing_inside
   = tc_lpats penv pats pat_tys thing_inside
   where
-    penv = PE { pe_res_tvs = tyVarsOfTypes (res_ty : pat_tys)
-              , pe_lazy = False
-              , pe_ctxt = LamPat ctxt }
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
 
 tcPat :: HsMatchContext Name
       -> LPat Name -> TcSigmaType 
-      -> TcRhoType             -- Result type
       -> TcM a                 -- Checker for body, given
                                -- its result type
       -> TcM (LPat TcId, a)
-tcPat ctxt pat pat_ty res_ty thing_inside
+tcPat ctxt pat pat_ty thing_inside
   = tc_lpat pat pat_ty penv thing_inside
   where
-    penv = PE { pe_res_tvs = tyVarsOfTypes [res_ty, pat_ty]
-              , pe_lazy = False
-              , pe_ctxt = LamPat ctxt }
+    penv = PE { pe_lazy = False, pe_ctxt = LamPat ctxt }
    
 
 -----------------
 data PatEnv
-  = PE { pe_res_tvs :: TcTyVarSet      
-                  -- For existential escape check; see Note [Existential check]
-                  -- Nothing <=> inside a "~"
-                  -- Just tvs <=> unification tvs free in the result
-                  --              (which should be made untouchable in
-                  --               any existentials we encounter in the pattern)
-
-       , pe_lazy :: Bool       -- True <=> lazy context, so no existentials allowed
+  = PE { pe_lazy :: Bool       -- True <=> lazy context, so no existentials allowed
        , pe_ctxt :: PatCtxt    -- Context in which the whole pattern appears
-    }
+       }
 
 data PatCtxt
   = LamPat   -- Used for lambdas, case etc
@@ -163,7 +149,7 @@ data TcSigInfo
 
 instance Outputable TcSigInfo where
     ppr (TcSigInfo { sig_id = id, sig_tvs = tyvars, sig_theta = theta, sig_tau = tau})
-        = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrow theta <+> ppr tau
+        = ppr id <+> ptext (sLit "::") <+> ppr tyvars <+> pprThetaArrowTy theta <+> ppr tau
 \end{code}
 
 Note [sig_tau may be polymorphic]
@@ -188,7 +174,7 @@ Note [Existential check]
 Lazy patterns can't bind existentials.  They arise in two ways:
   * Let bindings      let { C a b = e } in b
   * Twiddle patterns  f ~(C a b) = e
-The pe_res_tvs field of PatEnv says whether we are inside a lazy
+The pe_lazy field of PatEnv says whether we are inside a lazy
 pattern (perhaps deeply)
 
 If we aren't inside a lazy pattern then we can bind existentials,
@@ -207,7 +193,7 @@ res_ty free vars.
 %************************************************************************
 
 \begin{code}
-tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (CoercionI, TcId)
+tcPatBndr :: PatEnv -> Name -> TcSigmaType -> TcM (Coercion, TcId)
 -- (coi, xp) = tcPatBndr penv x pat_ty
 -- Then coi : pat_ty ~ typeof(xp)
 --
@@ -219,11 +205,11 @@ tcPatBndr (PE { pe_ctxt = LetPat lookup_sig no_gen}) bndr_name pat_ty
       
   | otherwise
   = do { bndr_id <- newNoSigLetBndr no_gen bndr_name pat_ty
-       ; return (IdCo pat_ty, bndr_id) }
+       ; return (mkReflCo pat_ty, bndr_id) }
 
 tcPatBndr (PE { pe_ctxt = _lam_or_proc }) bndr_name pat_ty
   = do { bndr <- mkLocalBinder bndr_name pat_ty
-       ; return (IdCo pat_ty, bndr) }
+       ; return (mkReflCo pat_ty, bndr) }
 
 ------------
 newSigLetBndr :: LetBndrSpec -> Name -> TcSigInfo -> TcM TcId
@@ -294,7 +280,7 @@ bindInstsOfPatId id thing_inside
   | not (isOverloadedTy (idType id))
   = do { res <- thing_inside; return (res, emptyTcEvBinds) }
   | otherwise
-  = do { (res, lie) <- getConstraints thing_inside
+  = do { (res, lie) <- captureConstraints thing_inside
        ; binds <- bindLocalMethods lie [id]
        ; return (res, binds) }
 -}
@@ -387,17 +373,7 @@ tc_pat     :: PatEnv
 tc_pat penv (VarPat name) pat_ty thing_inside
   = do { (coi, id) <- tcPatBndr penv name pat_ty
        ; res <- tcExtendIdEnv1 name id thing_inside
-        ; return (mkHsWrapPatCoI coi (VarPat id) pat_ty, res) }
-
-{- Need this if we re-add Method constraints 
-       ; (res, binds) <- bindInstsOfPatId id $
-                         tcExtendIdEnv1 name id $
-                         (traceTc (text "binding" <+> ppr name <+> ppr (idType id))
-                          >> thing_inside)
-       ; let pat' | isEmptyTcEvBinds binds = VarPat id
-                  | otherwise              = VarPatOut id binds
-       ; return (mkHsWrapPatCoI coi pat' pat_ty, res) }
--}
+        ; return (mkHsWrapPatCo coi (VarPat id) pat_ty, res) }
 
 tc_pat penv (ParPat pat) pat_ty thing_inside
   = do { (pat', res) <- tc_lpat pat pat_ty penv thing_inside
@@ -410,11 +386,12 @@ tc_pat penv (BangPat pat) pat_ty thing_inside
 tc_pat penv lpat@(LazyPat pat) pat_ty thing_inside
   = do { (pat', (res, pat_ct)) 
                <- tc_lpat pat pat_ty (makeLazy penv) $ 
-                  getConstraints thing_inside
+                  captureConstraints thing_inside
                -- Ignore refined penv', revert to penv
 
        ; emitConstraints pat_ct
-       -- getConstraints/extendConstraintss: see Note [Hopping the LIE in lazy patterns]
+       -- captureConstraints/extendConstraints: 
+        --   see Note [Hopping the LIE in lazy patterns]
 
        -- Check there are no unlifted types under the lazy pattern
        ; when (any (isUnLiftedType . idType) $ collectPatBinders pat') $
@@ -446,7 +423,7 @@ tc_pat penv (AsPat (L nm_loc name) pat) pat_ty thing_inside
            -- perhaps be fixed, but only with a bit more work.
            --
            -- If you fix it, don't forget the bindInstsOfPatIds!
-       ; return (mkHsWrapPatCoI coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
+       ; return (mkHsWrapPatCo coi (AsPat (L nm_loc bndr_id) pat') pat_ty, res) }
 
 tc_pat penv vpat@(ViewPat expr pat _) overall_pat_ty thing_inside 
   = do { checkUnboxedTuple overall_pat_ty $
@@ -471,7 +448,7 @@ tc_pat penv vpat@(ViewPat expr pat _) overall_pat_ty thing_inside
          -- pattern must have pat_ty
         ; (pat', res) <- tc_lpat pat pat_ty penv thing_inside
 
-       ; return (ViewPat (mkLHsWrapCoI expr_coi expr') pat' overall_pat_ty, res) }
+       ; return (ViewPat (mkLHsWrapCo expr_coi expr') pat' overall_pat_ty, res) }
 
 -- Type signatures in patterns
 -- See Note [Pattern coercions] below
@@ -534,7 +511,7 @@ tc_pat _ (LitPat simple_lit) pat_ty thing_inside
        ; coi <- unifyPatType lit_ty pat_ty
                -- coi is of kind: pat_ty ~ lit_ty
        ; res <- thing_inside 
-       ; return ( mkHsWrapPatCoI coi (LitPat simple_lit) pat_ty 
+       ; return ( mkHsWrapPatCo coi (LitPat simple_lit) pat_ty 
                  , res) }
 
 ------------------------
@@ -569,19 +546,19 @@ tc_pat penv (NPlusKPat (L nm_loc name) lit ge minus) pat_ty thing_inside
        ; instStupidTheta orig [mkClassPred icls [pat_ty']]     
     
        ; res <- tcExtendIdEnv1 name bndr_id thing_inside
-       ; return (mkHsWrapPatCoI coi pat' pat_ty, res) }
+       ; return (mkHsWrapPatCo coi pat' pat_ty, res) }
 
-tc_pat _ _other_pat _ _ = panic "tc_pat"       -- ConPatOut, SigPatOut, VarPatOut
+tc_pat _ _other_pat _ _ = panic "tc_pat"       -- ConPatOut, SigPatOut
 
 ----------------
-unifyPatType :: TcType -> TcType -> TcM CoercionI
+unifyPatType :: TcType -> TcType -> TcM Coercion
 -- In patterns we want a coercion from the
 -- context type (expected) to the actual pattern type
 -- But we don't want to reverse the args to unifyType because
 -- that controls the actual/expected stuff in error messages
 unifyPatType actual_ty expected_ty
   = do { coi <- unifyType actual_ty expected_ty
-       ; return (mkSymCoI coi) }
+       ; return (mkSymCo coi) }
 \end{code}
 
 Note [Hopping the LIE in lazy patterns]
@@ -593,7 +570,7 @@ We can't discharge the Num constraint from dictionaries bound by
 the pattern C!  
 
 So we have to make the constraints from thing_inside "hop around" 
-the pattern.  Hence the getConstraints and emitConstraints.
+the pattern.  Hence the captureConstraints and emitConstraints.
 
 The same thing ensures that equality constraints in a lazy match
 are not made available in the RHS of the match. For example
@@ -680,7 +657,7 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
   = do { data_con <- tcLookupDataCon con_name
        ; let tycon = dataConTyCon data_con
                  -- For data families this is the representation tycon
-             (univ_tvs, ex_tvs, eq_spec, eq_theta, dict_theta, arg_tys, _)
+             (univ_tvs, ex_tvs, eq_spec, theta, arg_tys, _)
                 = dataConFullSig data_con
 
          -- Instantiate the constructor type variables [a->ty]
@@ -692,10 +669,7 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
        ; setSrcSpan con_span $ addDataConStupidTheta data_con ctxt_res_tys
 
        ; checkExistentials ex_tvs penv 
-        ; let skol_info = case pe_ctxt penv of
-                            LamPat mc -> PatSkol data_con mc
-                            LetPat {} -> UnkSkol -- Doesn't matter
-       ; ex_tvs' <- tcInstSkolTyVars skol_info ex_tvs  
+        ; ex_tvs' <- tcInstSuperSkolTyVars ex_tvs
                      -- Get location from monad, not from ex_tvs
 
         ; let pat_ty' = mkTyConApp tycon ctxt_res_tys
@@ -705,9 +679,8 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
              tenv     = zipTopTvSubst (univ_tvs     ++ ex_tvs)
                                       (ctxt_res_tys ++ mkTyVarTys ex_tvs')
              arg_tys' = substTys tenv arg_tys
-             full_theta = eq_theta ++ dict_theta
 
-       ; if null ex_tvs && null eq_spec && null full_theta
+       ; if null ex_tvs && null eq_spec && null theta
          then do { -- The common case; no class bindings etc 
                     -- (see Note [Arrows and patterns])
                    (arg_pats', res) <- tcConArgs data_con arg_tys' 
@@ -723,29 +696,23 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
          else do   -- The general case, with existential, 
                     -- and local equality constraints
        { let eq_preds = [mkEqPred (mkTyVarTy tv, ty) | (tv, ty) <- eq_spec]
-             theta'   = substTheta tenv (eq_preds ++ full_theta)
+             theta'   = substTheta tenv (eq_preds ++ theta)
                            -- order is *important* as we generate the list of
                            -- dictionary binders from theta'
              no_equalities = not (any isEqPred theta')
-
+              skol_info = case pe_ctxt penv of
+                            LamPat mc -> PatSkol data_con mc
+                            LetPat {} -> UnkSkol -- Doesn't matter
         ; gadts_on <- xoptM Opt_GADTs
        ; checkTc (no_equalities || gadts_on)
                  (ptext (sLit "A pattern match on a GADT requires -XGADTs"))
                  -- Trac #2905 decided that a *pattern-match* of a GADT
                  -- should require the GADT language flag
 
-       ; given <- newEvVars theta'
-        ; let free_tvs = pe_res_tvs penv
-               -- Since we have done checkExistentials,
-               -- pe_res_tvs can only be Just at this point
-               --
-               -- Nor do we need pat_ty, because we've put all the
-               -- unification variables in right at the start when
-               -- initialising the PatEnv; and the pattern itself
-               -- only adds skolems.
-
+        ; given <- newEvVars theta'
         ; (ev_binds, (arg_pats', res))
-            <- checkConstraints skol_info free_tvs ex_tvs' given $
+            <- checkConstraints skol_info ex_tvs' given $
                 tcConArgs data_con arg_tys' arg_pats penv thing_inside
 
         ; let res_pat = ConPatOut { pat_con   = L con_span data_con, 
@@ -758,21 +725,21 @@ tcConPat penv (L con_span con_name) pat_ty arg_pats thing_inside
        } }
 
 ----------------------------
-matchExpectedPatTy :: (TcRhoType -> TcM (CoercionI, a))
+matchExpectedPatTy :: (TcRhoType -> TcM (Coercion, a))
                     -> TcRhoType -> TcM (HsWrapper, a) 
 -- See Note [Matching polytyped patterns]
 -- Returns a wrapper : pat_ty ~ inner_ty
 matchExpectedPatTy inner_match pat_ty
   | null tvs && null theta
   = do { (coi, res) <- inner_match pat_ty
-       ; return (coiToHsWrapper (mkSymCoI coi), res) }
+       ; return (coToHsWrapper (mkSymCo coi), res) }
                 -- The Sym is because the inner_match returns a coercion
         -- that is the other way round to matchExpectedPatTy
 
   | otherwise
   = do { (_, tys, subst) <- tcInstTyVars tvs
        ; wrap1 <- instCall PatOrigin tys (substTheta subst theta)
-       ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (substTy subst tau)
+       ; (wrap2, arg_tys) <- matchExpectedPatTy inner_match (TcType.substTy subst tau)
        ; return (wrap2 <.> wrap1 , arg_tys) }
   where
     (tvs, theta, tau) = tcSplitSigmaTy pat_ty
@@ -781,7 +748,7 @@ matchExpectedPatTy inner_match pat_ty
 matchExpectedConTy :: TyCon     -- The TyCon that this data 
                                 -- constructor actually returns
                   -> TcRhoType  -- The type of the pattern
-                  -> TcM (CoercionI, [TcSigmaType])
+                  -> TcM (Coercion, [TcSigmaType])
 -- See Note [Matching constructor patterns]
 -- Returns a coercion : T ty1 ... tyn ~ pat_ty
 -- This is the same way round as matchExpectedListTy etc
@@ -796,10 +763,10 @@ matchExpectedConTy data_tc pat_ty
        ; coi1 <- unifyType (mkTyConApp fam_tc (substTys subst fam_args)) pat_ty
                     -- coi1 : T (ty1,ty2) ~ pat_ty
 
-       ; let coi2 = ACo (mkTyConApp co_tc tys)
+       ; let coi2 = mkAxInstCo co_tc tys
                     -- coi2 : T (ty1,ty2) ~ T7 ty1 ty2
 
-       ; return (mkTransCoI (mkSymCoI coi2) coi1, tys) }
+       ; return (mkTransCo (mkSymCo coi2) coi1, tys) }
 
   | otherwise
   = matchExpectedTyConApp data_tc pat_ty