-
-%************************************************************************
-%* *
- Type refinement
-%* *
-%************************************************************************
-
-\begin{code}
-refineAlt :: DataCon -- For tracing only
- -> PatState
- -> [TcTyVar] -- Existentials
- -> [CoVar] -- Equational constraints
- -> BoxySigmaType -- Pattern type
- -> TcM PatState
-
-refineAlt con pstate ex_tvs [] pat_ty
- | null $ dataConEqTheta con
- = return pstate -- Common case: no equational constraints
-
-refineAlt con pstate ex_tvs co_vars pat_ty
- = do { opt_gadt <- doptM Opt_GADTs -- No type-refinement unless GADTs are on
- ; if (not opt_gadt) then return pstate
- else do
-
- { checkTc (isRigidTy pat_ty) (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
-
- -- 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, pat_eqs = (pat_eqs pstate || not (null $ dataConEqTheta con)) }) }
- -- DO NOT refine the envt right away, because we
- -- might be inside a lazy pattern. Instead, refine pstate
- where
-
- trace_msg = text "refineAlt:match" <+>
- vcat [ ppr con <+> ppr ex_tvs,
- ppr [(v, tyVarKind v) | v <- co_vars],
- ppr reft]
- } } }
-\end{code}
+Note [Arrows and patterns]
+~~~~~~~~~~~~~~~~~~~~~~~~~~
+(Oct 07) Arrow noation has the odd property that it involves "holes in the scope".
+For example:
+ expr :: Arrow a => a () Int
+ expr = proc (y,z) -> do
+ x <- term -< y
+ expr' -< x
+
+Here the 'proc (y,z)' binding scopes over the arrow tails but not the
+arrow body (e.g 'term'). As things stand (bogusly) all the
+constraints from the proc body are gathered together, so constraints
+from 'term' will be seen by the tcPat for (y,z). But we must *not*
+bind constraints from 'term' here, becuase the desugarer will not make
+these bindings scope over 'term'.
+
+The Right Thing is not to confuse these constraints together. But for
+now the Easy Thing is to ensure that we do not have existential or
+GADT constraints in a 'proc', and to short-cut the constraint
+simplification for such vanilla patterns so that it binds no
+constraints. Hence the 'fast path' in tcConPat; but it's also a good
+plan for ordinary vanilla patterns to bypass the constraint
+simplification step.