Commit b5c81203 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Complete the fix for #13441 (pattern synonyms)

Do not attempt to typecheck both directions of an
implicitly-bidirectional pattern synonym simultanously,
as we were before.  Instead, the builder is typechecked
when we typecheck the code for the builder, which was
of course happening already, even in both bidirectional
cases.

See Note [Checking against a pattern signature], under
"Existential type variables".
parent cea71418
......@@ -149,14 +149,11 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
pushLevelAndCaptureConstraints $
tcExtendTyVarEnv univ_tvs $
tcPat PatSyn lpat (mkCheckExpType pat_ty) $
do { let new_tv = case dir of
ImplicitBidirectional -> newMetaSigTyVarX
_ -> newMetaTyVarX
-- new_tv: see the "Existential type variables"
-- part of Note [Checking against a pattern signature]
in_scope = mkInScopeSet (mkVarSet univ_tvs)
do { let in_scope = mkInScopeSet (mkVarSet univ_tvs)
empty_subst = mkEmptyTCvSubst in_scope
; (subst, ex_tvs') <- mapAccumLM new_tv empty_subst ex_tvs
; (subst, ex_tvs') <- mapAccumLM newMetaTyVarX empty_subst ex_tvs
-- newMetaTyVarX: see the "Existential type variables"
-- part of Note [Checking against a pattern signature]
; traceTc "tcpatsyn1" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs])
; traceTc "tcpatsyn2" (vcat [ ppr v <+> dcolon <+> ppr (tyVarKind v) | v <- ex_tvs'])
; let prov_theta' = substTheta subst prov_theta
......@@ -241,20 +238,26 @@ unify x := [a] during type checking, and then use the instantiating type
dl = $dfunEqList d
in k [a] dl ys
This "concealing" story works for /uni-directional/ pattern synonyms.
It also works for /explicitly-bidirectional/ pattern synonyms, where
the constructor direction is typecheked entirely separately.
But for /implicitly-bidirecitonal/ ones like
pattern P x = MkS x
we are trying to typecheck both directions at once. So for this we
use SigTv, rather than a generic TauTv. But it's not quite done:
- We should really check that those SigTvs don't get unified
with each other.
- Trac #13441 is rejected if you use an implicitly-bidirectional
pattern.
Maybe it'd be better to treat it like an explicitly-bidirectional
pattern?
All this applies when type-checking the /matching/ side of
a pattern synonym. What about the /building/ side?
* For Unidirectional, there is no builder
* For ExplicitBidirectional, the builder is completely separate
code, typechecked in tcPatSynBuilderBind
* For ImplicitBidirectional, the builder is still typechecked in
tcPatSynBuilderBind, by converting the pattern to an expression and
typechecking it.
At one point, for ImplicitBidirectional I used SigTvs (instead of
TauTvs) in tcCheckPatSynDecl. But (a) strengthening the check here
is redundant since tcPatSynBuilderBind does the job, (b) it was
still incomplete (SigTvs can unify with each other), and (c) it
didn't even work (Trac #13441 was accepted with
ExplicitBidirectional, but rejected if expressed in
ImplicitBidirectional form. Conclusion: trying to be too clever is
a bad idea.
-}
collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
......
......@@ -21,9 +21,16 @@ type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
type Vec n a = FList Identity (Replicate n a)
-- Using explicitly-bidirectional pattern
pattern (:>) :: forall n a. n ~ Length (Replicate n a)
=> forall m. n ~ Succ m
=> a -> Vec m a -> Vec n a
pattern x :> xs <- Identity x :@ xs
where
x :> xs = Identity x :@ xs
-- Using implicitly-bidirectional pattern
pattern (:>>) :: forall n a. n ~ Length (Replicate n a)
=> forall m. n ~ Succ m
=> a -> Vec m a -> Vec n a
pattern x :>> xs = Identity x :@ xs
{-# LANGUAGE PatternSynonyms, GADTs #-}
module T13441a where
data S where
MkS :: Eq a => [a] -> S
-- Unidirectional pattern binding;
-- the existential is more specific than needed
-- c.f. T13441b
pattern P :: () => Eq x => x -> S
pattern P x <- MkS x
{-# LANGUAGE PatternSynonyms, GADTs #-}
module T13441a where
data S where
MkS :: Eq a => [a] -> S
-- Implicitly-bidirectional pattern binding;
-- the existential is more specific than needed,
-- and hence should be rejected
-- c.f. T13441a
pattern P :: () => Eq x => x -> S
pattern P x = MkS x
T13441b.hs:12:19: error:
• Couldn't match expected type ‘[a0]’ with actual type ‘x’
‘x’ is a rigid type variable bound by
the signature for pattern synonym ‘P’ at T13441b.hs:12:1-19
• In the first argument of ‘MkS’, namely ‘x’
In the expression: MkS x
In an equation for ‘P’: P x = MkS x
• Relevant bindings include
x :: x (bound at T13441b.hs:12:19)
$bP :: x -> S (bound at T13441b.hs:12:9)
......@@ -65,3 +65,5 @@ test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
test('T12968', normal, compile, [''])
test('T13349b', normal, compile, [''])
test('T13441', normal, compile, [''])
test('T13441a', normal, compile, [''])
test('T13441b', normal, compile_fail, [''])
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment