Commit 7c7479d0 authored by Simon Peyton Jones's avatar Simon Peyton Jones

Fix explicitly-bidirectional pattern synonyms

This partly fixes Trac #13441, at least for the explicitly
bidirectional case.

See Note [Checking against a pattern signature], the part about
"Existential type variables".

Alas, the implicitly-bidirectional case is still not quite right, but
at least there is a workaround by making it explicitly bidirectional.
parent 7e1c492d
......@@ -149,13 +149,14 @@ 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 | isUnidirectional dir = newMetaTyVarX
| otherwise = newMetaSigTyVarX
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)
empty_subst = mkEmptyTCvSubst in_scope
; (subst, ex_tvs') <- mapAccumLM new_tv empty_subst ex_tvs
-- 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
......@@ -240,12 +241,20 @@ 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,
but obviously not for bidirectional ones. So in the bidirectional case
we use SigTv, rather than a generic TauTv, meta-tyvar so that. And
we should really check that those SigTvs don't get unified with each
other.
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?
-}
collectPatSynArgInfo :: HsPatSynDetails (Located Name) -> ([Name], [Name], Bool)
......@@ -519,7 +528,6 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
| Right match_group <- mb_match_group -- Bidirectional
= do { patsyn <- tcLookupPatSyn name
; traceTc "tcPatSynBuilderBind {" $ ppr patsyn
; let Just (builder_id, need_dummy_arg) = patSynBuilder patsyn
-- Bidirectional, so patSynBuilder returns Just
......@@ -534,6 +542,8 @@ tcPatSynBuilderBind (PSB { psb_id = L loc name, psb_def = lpat
sig = completeSigFromId (PatSynCtxt name) builder_id
; traceTc "tcPatSynBuilderBind {" $
ppr patsyn $$ ppr builder_id <+> dcolon <+> ppr (idType builder_id)
; (builder_binds, _) <- tcPolyCheck emptyPragEnv sig (noLoc bind)
; traceTc "tcPatSynBuilderBind }" $ ppr builder_binds
; return builder_binds }
......
{-# LANGUAGE ScopedTypeVariables, PatternSynonyms, DataKinds, PolyKinds,
GADTs, TypeOperators, TypeFamilies #-}
module T13441 where
import Data.Functor.Identity
data FList f xs where
FNil :: FList f '[]
(:@) :: f x -> FList f xs -> FList f (x ': xs)
data Nat = Zero | Succ Nat
type family Length (xs :: [k]) :: Nat where
Length '[] = Zero
Length (_ ': xs) = Succ (Length xs)
type family Replicate (n :: Nat) (x :: a) = (r :: [a]) where
Replicate Zero _ = '[]
Replicate (Succ n) x = x ': Replicate n x
type Vec n a = FList Identity (Replicate n a)
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
......@@ -64,3 +64,4 @@ test('T12698', normal, compile, [''])
test('T12746', normal, multi_compile, ['T12746', [('T12746A.hs', '-c')],'-v0'])
test('T12968', normal, compile, [''])
test('T13349b', normal, compile, [''])
test('T13441', normal, compile, [''])
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