diff options
author | Simon Peyton Jones <simonpj@microsoft.com> | 2018-01-04 17:18:15 +0000 |
---|---|---|
committer | Simon Peyton Jones <simonpj@microsoft.com> | 2018-01-04 17:24:10 +0000 |
commit | 307d1dfe1d705379eafad6dba65e651ae3465cda (patch) | |
tree | 93a87a622191dbddf410c07eac3f94229d7a29ac | |
parent | 86ea3b1e261ad59dfa7ac13d422a4d657dc83e92 (diff) | |
download | haskell-307d1dfe1d705379eafad6dba65e651ae3465cda.tar.gz |
Fix deep, dark corner of pattern synonyms
Trac #14552 showed a very obscure case where we can't infer a
good pattern-synonym type.
The error message is horrible, but at least we no longer crash
and burn.
-rw-r--r-- | compiler/typecheck/TcPatSyn.hs | 50 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T14552.hs | 43 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/T14552.stderr | 9 | ||||
-rw-r--r-- | testsuite/tests/patsyn/should_fail/all.T | 1 |
4 files changed, 103 insertions, 0 deletions
diff --git a/compiler/typecheck/TcPatSyn.hs b/compiler/typecheck/TcPatSyn.hs index 7e21af5faa..0086a83367 100644 --- a/compiler/typecheck/TcPatSyn.hs +++ b/compiler/typecheck/TcPatSyn.hs @@ -91,6 +91,12 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, univ_tvs = filterOut (`elemVarSet` ex_tv_set) qtvs req_theta = map evVarPred req_dicts + -- See Note [Type variables whose kind is captured] + ; let bad_tvs = [ tv | tv <- univ_tvs + , tyCoVarsOfType (tyVarKind tv) + `intersectsVarSet` ex_tv_set ] + ; mapM_ (badUnivTv ex_tvs) bad_tvs + ; prov_dicts <- mapM zonkId prov_dicts ; let filtered_prov_dicts = mkMinimalBySCs evVarPred prov_dicts prov_theta = map evVarPred filtered_prov_dicts @@ -105,6 +111,19 @@ tcInferPatSynDecl PSB{ psb_id = lname@(L _ name), psb_args = details, (map nlHsVar args, map idType args) pat_ty rec_fields } +badUnivTv :: [TyVar] -> TyVar -> TcM () +badUnivTv ex_tvs bad_tv + = addErrTc $ + vcat [ text "Universal type variable" <+> quotes (ppr bad_tv) + <+> text "has existentially bound kind:" + , nest 2 (ppr_with_kind bad_tv) + , hang (text "Existentially-bound variables:") + 2 (vcat (map ppr_with_kind ex_tvs)) + , text "Probable fix: give the pattern synoym a type signature" + ] + where + ppr_with_kind tv = ppr tv <+> dcolon <+> ppr (tyVarKind tv) + {- Note [Remove redundant provided dicts] ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Recall that @@ -126,6 +145,37 @@ Similarly consider The pattern (Bam x y) binds two (Ord a) dictionaries, but we only need one. Agian mkMimimalWithSCs removes the redundant one. + +Note [Type variables whose kind is captured] +~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ +Consider + data AST a = Sym [a] + class Prj s where { prj :: [a] -> Maybe (s a) + pattern P x <= Sym (prj -> Just x) + +Here we get a matcher with this type + $mP :: forall s a. Prj s => AST a -> (s a -> r) -> r -> r + +No problem. But note that 's' is not fixed by the type of the +pattern (AST a), nor is it existentially bound. It's really only +fixed by the type of the continuation. + +Trac #14552 showed that this can go wrong if the kind of 's' mentions +existentially bound variables. We obviously can't make a type like + $mP :: forall (s::k->*) a. Prj s => AST a -> (forall k. s a -> r) + -> r -> r +But neither is 's' itself existentially bound, so the forall (s::k->*) +can't go in the inner forall either. (What would the matcher apply +the continuation to?) + +So we just fail in this case, with a pretty terrible error message. +Maybe we could do better, but I can't see how. (It'd be possible to +default 's' to (Any k), but that probably isn't what the user wanted, +and it not straightforward to implement, because by the time we see +the problem, simplifyInfer has already skolemised 's'.) + +This stuff can only happen in the presence of view patterns, with +TypeInType, so it's a bit of a corner case. -} tcCheckPatSynDecl :: PatSynBind GhcRn GhcRn diff --git a/testsuite/tests/patsyn/should_fail/T14552.hs b/testsuite/tests/patsyn/should_fail/T14552.hs new file mode 100644 index 0000000000..77f08575b1 --- /dev/null +++ b/testsuite/tests/patsyn/should_fail/T14552.hs @@ -0,0 +1,43 @@ +{-# Language RankNTypes, ViewPatterns, PatternSynonyms, TypeOperators, ScopedTypeVariables, + KindSignatures, PolyKinds, DataKinds, TypeFamilies, TypeInType, GADTs #-} + +module T14552 where + +import Data.Kind +import Data.Proxy + +data family Sing a + +type a --> b = (a, b) -> Type + +type family F (f::a --> b) (x::a) :: b + +newtype Limit :: (k --> Type) -> Type where + Limit :: (forall xx. Proxy xx -> F f xx) -> Limit f + +data Exp :: [Type] -> Type -> Type where + TLam :: (forall aa. Proxy aa -> Exp xs (F w aa)) + -> Exp xs (Limit w) + +pattern FOO f <- TLam (($ Proxy) -> f) + + +{- +TLam :: forall (xs::[Type]) (b::Type). -- Universal + forall k (w :: k --> Type). -- Existential + (b ~ Limit w) => + => (forall (aa :: k). Proxy aa -> Exp xs (F w aa)) + -> Exp xs b + +-} + +{- +mfoo :: Exp xs b + -> (forall k (w :: k --> Type). + (b ~ Limit w) + => Exp xs (F w aa) + -> r) + -> r +mfoo scrut k = case srcut of + TLam g -> k (g Proxy) +-} diff --git a/testsuite/tests/patsyn/should_fail/T14552.stderr b/testsuite/tests/patsyn/should_fail/T14552.stderr new file mode 100644 index 0000000000..1ead6443b4 --- /dev/null +++ b/testsuite/tests/patsyn/should_fail/T14552.stderr @@ -0,0 +1,9 @@ + +T14552.hs:22:9: error: + • Universal type variable ‘aa’ has existentially bound kind: + aa :: k + Existentially-bound variables: + k :: * + w :: k --> * + Probable fix: give the pattern synoym a type signature + • In the declaration for pattern synonym ‘FOO’ diff --git a/testsuite/tests/patsyn/should_fail/all.T b/testsuite/tests/patsyn/should_fail/all.T index 4bf631f982..d2985d5e14 100644 --- a/testsuite/tests/patsyn/should_fail/all.T +++ b/testsuite/tests/patsyn/should_fail/all.T @@ -40,3 +40,4 @@ test('T14112', normal, compile_fail, ['']) test('T14114', normal, compile_fail, ['']) test('T14380', normal, compile_fail, ['']) test('T14498', normal, compile_fail, ['']) +test('T14552', normal, compile_fail, ['']) |