diff options
| -rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 45 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T13441.hs | 7 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T13441a.hs | 11 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T13441b.hs | 12 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/T13441b.stderr | 11 | ||||
| -rw-r--r-- | testsuite/tests/patsyn/should_compile/all.T | 2 |
6 files changed, 67 insertions, 21 deletions
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 6f7764eb3a..01cb5420fd 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -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) diff --git a/testsuite/tests/patsyn/should_compile/T13441.hs b/testsuite/tests/patsyn/should_compile/T13441.hs index d7a339f782..738017500d 100644 --- a/testsuite/tests/patsyn/should_compile/T13441.hs +++ b/testsuite/tests/patsyn/should_compile/T13441.hs @@ -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 diff --git a/testsuite/tests/patsyn/should_compile/T13441a.hs b/testsuite/tests/patsyn/should_compile/T13441a.hs new file mode 100644 index 0000000000..77360946a2 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T13441a.hs @@ -0,0 +1,11 @@ +{-# 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 diff --git a/testsuite/tests/patsyn/should_compile/T13441b.hs b/testsuite/tests/patsyn/should_compile/T13441b.hs new file mode 100644 index 0000000000..8f8d2ba5ca --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T13441b.hs @@ -0,0 +1,12 @@ +{-# 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 diff --git a/testsuite/tests/patsyn/should_compile/T13441b.stderr b/testsuite/tests/patsyn/should_compile/T13441b.stderr new file mode 100644 index 0000000000..4469086c82 --- /dev/null +++ b/testsuite/tests/patsyn/should_compile/T13441b.stderr @@ -0,0 +1,11 @@ + +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) diff --git a/testsuite/tests/patsyn/should_compile/all.T b/testsuite/tests/patsyn/should_compile/all.T index 1f36424640..8fce7e987d 100644 --- a/testsuite/tests/patsyn/should_compile/all.T +++ b/testsuite/tests/patsyn/should_compile/all.T @@ -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, ['']) |