#11224: Program doesn't preserve semantics after pattern synonym inlining. -------------------------------------+------------------------------------- Reporter: anton.dubovik | Owner: Type: bug | Status: new Priority: highest | Milestone: 8.0.1 Component: Compiler | Version: 7.10.2 Resolution: | Keywords: | PatternSynonyms Operating System: Windows | Architecture: x86_64 Type of failure: Incorrect result | (amd64) at runtime | Test Case: Blocked By: | Blocking: Related Tickets: #11225 | Differential Rev(s): Phab:D1632 Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): Right. To typecheck a program involving `P` we absolutely need to know the universal/existential split. Above, I was thinking that we could use the pattern type signature to specify the "shape" of the type, but work out the univ/existential split from the definition itself. A bit like a type with wildcards. But that would mean that you could not typecheck uses of a pattern synonym solely from its signature; because the signature does not say enough. Like wildcards, inference would be involved. But that's obviously unsatisfactory; for example, you could not put a pattern synonym signature in a hs-boot file. So, if we want signatures to be fully precise (i.e. say everything), and I think that is a solidly good goal, we'd need to require the user to specify the required/provided split for type variables too. Terminology: * "Universal" for type variables lines up with "required" for the constraints * "Existential" for type variables lines up with "provided" for the constraints Now, we need syntax for expressing the split. I suppose we can use the same nested structure as we do for required/provided, like this: {{{ pattern type P1 :: forall a. a -> T a -- a is universal pattern type P2 :: forall a. Eq a => a -> T -- a is universal, (Eq a) is required pattern type P3 :: forall a. Eq a => -- a is universal, (Eq a) is required forall b. a -> b -> T a -- b is existential pattern type P3 :: forall a. Eq a => -- a is universal, (Eq a) is required forall b. Ord b => -- b is existential, (Ord b) is provided a -> b -> T a }}} Note: * I think we could safely leave out the leading (universal) `forall`, in the usual way. That is, the free vars of the entire type are considered universal. * You can never leave out the existential forall, if it binds any variables. * How can you distinguish the existential forall if the universal forall and context are absent? Only by putting in the universal forall or the required context; e.g. {{{ pattern type P5 :: forall. forall b. b -> T pattern type P6 :: () => forall b. b -> T }}} The only downside of this is that you might say that given {{{ pattern type P :: a -> (a->Int) -> T }}} the `a` is almost certain to be existential. After all this is the type we'd give to a data constructor: {{{ data T where MkT :: (a->Int) -> a -> T }}} So why do we need explicitly-specified existentials in a pattern synonym, but not in a data constructor? Because a view pattern could make it universal. Degenerately in this case: {{{ pattern Q :: a -> (a->Int) -> String pattern Q x y <- (odd_fun -> (x,y)) odd_fun :: String -> (a, a->Int) odd_fun _ = (undefined, const 2) }}} Conclusion: we need the possibility of explicitly-specified existentials. However, rather than insisting that you always specify the existential forall, here is a rule that would catch the common cases: if you don't specify the existential `forall`, you get: * the free vars of the arg-tys * plus the free vars of the provided constraints (if any), * minus * the universal forall'd vars, if there is a universal `forall` * or the free vars of the result ty, plus required constraints (if any), otherwise If neither `forall` is given, we compute the existential variables using the above rule; then the universals are the remaining free variables. So in the signatures that started this ticket {{{ pattern Q1 :: () => Read a => a -> String pattern Q2 :: Read a => a -> String }}} would behave as if you had written {{{ pattern Q1 :: () => forall a. Read a => a -> String pattern Q2 :: forall a. Read a => a -> String }}} The advantage of this rule is that is allows you to omit both `forall`s in all but the most degenerate cases like `Q` above. How does that sound? I think it is more or less what Richard was proposing in comment:8, but it's taken me a while to catch up. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/11224#comment:24 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler