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

Pattern synonyms and higher rank types

This patch fixes two separate bugs which contributed to making
Trac #13752 go wrong

1.  We need to use tcSubType, not tcUnify,
    in tcCheckPatSynDecl.tc_arg.

    Reason: Note [Pattern synonyms and higher rank types]

2.  TcUnify.tc_sub_type had a special case designed to improve error
    messages; see Note [Don't skolemise unnecessarily].  But the
    special case was too liberal, and ended up using unification
    (which led to rejecting the program) when it should instead taken
    the normal path (which accepts the program).

    I fixed this by making the test more conservative.
parent 10131947
......@@ -192,12 +192,26 @@ tcCheckPatSynDecl psb@PSB{ psb_id = lname@(L _ name), psb_args = details
= do { -- Look up the variable actually bound by lpat
-- and check that it has the expected type
arg_id <- tcLookupId arg_name
; coi <- unifyType (Just arg_id)
(idType arg_id)
(substTyUnchecked subst arg_ty)
; return (mkLHsWrapCo coi $ nlHsVar arg_id) }
; wrap <- tcSubType_NC GenSigCtxt
(idType arg_id)
(substTyUnchecked subst arg_ty)
-- Why do we need tcSubType here?
-- See Note [Pattern synonyms and higher rank types]
; return (mkLHsWrap wrap $ nlHsVar arg_id) }
{- [Pattern synonyms and higher rank types]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Consider
data T = MkT (forall a. a->a)
pattern P :: (Int -> Int) -> T
pattern P x <- MkT x
This should work. But in the matcher we must match against MkT, and then
instantiate its argument 'x', to get a functino of type (Int -> Int).
Equality is not enough! Trac #13752 was an example.
{- Note [Checking against a pattern signature]
Note [Checking against a pattern signature]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
When checking the actual supplied pattern against the pattern synonym
signature, we need to be quite careful.
......
......@@ -638,8 +638,8 @@ tc_sub_tc_type :: CtOrigin -- used when calling uType
-- If wrap = tc_sub_type t1 t2
-- => wrap :: t1 ~> t2
tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
| is_poly ty_expected -- See Note [Don't skolemise unnecessarily]
, not (is_poly ty_actual)
| definitely_poly ty_expected -- See Note [Don't skolemise unnecessarily]
, not (possibly_poly ty_actual)
= do { traceTc "tc_sub_tc_type (drop to equality)" $
vcat [ text "ty_actual =" <+> ppr ty_actual
, text "ty_expected =" <+> ppr ty_expected ]
......@@ -656,13 +656,21 @@ tc_sub_tc_type eq_orig inst_orig ctxt ty_actual ty_expected
ty_actual sk_rho
; return (sk_wrap <.> inner_wrap) }
where
is_poly ty
possibly_poly ty
| isForAllTy ty = True
| Just (_, res) <- splitFunTy_maybe ty = is_poly res
| Just (_, res) <- splitFunTy_maybe ty = possibly_poly res
| otherwise = False
-- NB *not* tcSplitFunTy, because here we want
-- to decompose type-class arguments too
definitely_poly ty
| (tvs, theta, tau) <- tcSplitSigmaTy ty
, (tv:_) <- tvs
, null theta
, isInsolubleOccursCheck NomEq tv tau
= True
| otherwise
= False
{- Note [Don't skolemise unnecessarily]
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
......@@ -674,11 +682,31 @@ error. It's better to say that
(Char->Char) ~ (forall a. a->a)
fails.
In general,
* if the RHS type an outermost forall (i.e. skolemisation
is the next thing we'd do)
* and the LHS has no top-level polymorphism (but looking deeply)
then we can revert to simple equality.
So roughly:
* if the ty_expected has an outermost forall
(i.e. skolemisation is the next thing we'd do)
* and the ty_actual has no top-level polymorphism (but looking deeply)
then we can revert to simple equality. But we need to be careful.
These examples are allfine:
* (Char -> forall a. a->a) <= (forall a. Char -> a -> a)
Polymorphism is buried in ty_actual
* (Char->Char) <= (forall a. Char -> Char)
ty_expected isn't really polymorphic
* (Char->Char) <= (forall a. (a~Char) => a -> a)
ty_expected isn't really polymorphic
* (Char->Char) <= (forall a. F [a] Char -> Char)
where type instance F [x] t = t
ty_expected isn't really polymorphic
If we prematurely go to equality we'll reject a program we should
accept (e.g. Grac #13752). So the test (which is only to improve
error messagse) is very conservative:
* ty_actual is /definitely/ monomorphic
* ty_expected is /definitely/ polymorphic
-}
---------------
......
{-# LANGUAGE TypeFamilies, ConstraintKinds, PatternSynonyms, RankNTypes #-}
module T13752 where
newtype Arrange = Arrange {getArrange :: [Int] -> [Int]}
pattern Heh :: (c ~ ((~) Int)) => (forall a. c a => [a] -> [a]) -> Arrange
-- pattern Heh :: (forall a. (Int ~ a) => [a] -> [a]) -> Arrange
pattern Heh f <- Arrange f
{-# LANGUAGE PatternSynonyms, RankNTypes #-}
module T13752a where
data T = MkT (forall a. a->a)
pattern P :: (Int -> Int) -> T
pattern P x <- MkT x
......@@ -68,3 +68,5 @@ test('T13441', normal, compile, [''])
test('T13441a', normal, compile, [''])
test('T13441b', normal, compile_fail, [''])
test('T13454', normal, compile, [''])
test('T13752', normal, compile, [''])
test('T13752a', 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