-
-%************************************************************************
-%* *
- 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
- = 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" <+>
- vcat [ ppr con <+> ppr ex_tvs,
- ppr [(v, tyVarKind v) | v <- co_vars],
- ppr reft]
- }
-\end{code}
-
-
-%************************************************************************
-%* *
- Overloaded literals
-%* *
-%************************************************************************
-
-In tcOverloadedLit we convert directly to an Int or Integer if we
-know that's what we want. This may save some time, by not
-temporarily generating overloaded literals, but it won't catch all
-cases (the rest are caught in lookupInst).
-
-\begin{code}
-tcOverloadedLit :: InstOrigin
- -> HsOverLit Name
- -> BoxyRhoType
- -> TcM (HsOverLit TcId)
-tcOverloadedLit orig lit@(HsIntegral i fi) res_ty
- | not (fi `isHsVar` fromIntegerName) -- Do not generate a LitInst for rebindable syntax.
- -- Reason: If we do, tcSimplify will call lookupInst, which
- -- will call tcSyntaxName, which does unification,
- -- which tcSimplify doesn't like
- -- ToDo: noLoc sadness
- = do { integer_ty <- tcMetaTy integerTyConName
- ; fi' <- tcSyntaxOp orig fi (mkFunTy integer_ty res_ty)
- ; return (HsIntegral i (HsApp (noLoc fi') (nlHsLit (HsInteger i integer_ty)))) }
-
- | Just expr <- shortCutIntLit i res_ty
- = return (HsIntegral i expr)
-
- | otherwise
- = do { expr <- newLitInst orig lit res_ty
- ; return (HsIntegral i expr) }
-
-tcOverloadedLit orig lit@(HsFractional r fr) res_ty
- | not (fr `isHsVar` fromRationalName) -- c.f. HsIntegral case
- = do { rat_ty <- tcMetaTy rationalTyConName
- ; fr' <- tcSyntaxOp orig fr (mkFunTy rat_ty res_ty)
- -- Overloaded literals must have liftedTypeKind, because
- -- we're instantiating an overloaded function here,
- -- whereas res_ty might be openTypeKind. This was a bug in 6.2.2
- -- However this'll be picked up by tcSyntaxOp if necessary
- ; return (HsFractional r (HsApp (noLoc fr') (nlHsLit (HsRat r rat_ty)))) }
-
- | Just expr <- shortCutFracLit r res_ty
- = return (HsFractional r expr)
-
- | otherwise
- = do { expr <- newLitInst orig lit res_ty
- ; return (HsFractional r expr) }
-
-newLitInst :: InstOrigin -> HsOverLit Name -> BoxyRhoType -> TcM (HsExpr TcId)
-newLitInst orig lit res_ty -- Make a LitInst
- = do { loc <- getInstLoc orig
- ; res_tau <- zapToMonotype res_ty
- ; new_uniq <- newUnique
- ; let lit_nm = mkSystemVarName new_uniq FSLIT("lit")
- lit_inst = LitInst lit_nm lit res_tau loc
- ; extendLIE lit_inst
- ; return (HsVar (instToId lit_inst)) }
-\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.