#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): An important question here is: should we do this at all? If I have my way and Dependent Haskell comes along, then types and terms will be the same. And we already have term patterns! -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:1 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I was thinking only of a counterpart to `Type`, not `HsType`. Your comment about type-level as-patterns is a good observation. It may be worth considering the situation in terms: Currently both patterns and expressions are parsed as expressions. (I believe there is some scenario where the parser can't be sure what it's looking at until it's too late. Maybe top-level TH splices. Maybe something more fundamental. The details aren't important here.) Then, another pass converts the expressions to patterns, erroring if the parsed expression doesn't form a pattern. Then, expressions and patterns are renamed and typechecked in different algorithms (mutually recursive ones, of course). Why have `HsPat` distinct from `HsExpr`? One reason I can think of is that `HsPat` is renamed very differently than `HsExpr` is: the former brings variables into scope, while the latter uses variables already in scope. The situation is a bit different in types. In particular, variable usages in type patterns do ''not'' bring those variables into scope. Instead, GHC looks through a type pattern before renaming it, gathers its free variables, and brings them into scope. This is subtly different than just having the variable occurrences bring them into scope, but it allows non- linear patterns, for example. I don't yet see a compelling reason for `HsTyPat`. If you want as- patterns, then we add a new constructor to `HsType`. As-patterns are rejected from the normal type kind-checker but accepted in the type pattern kind-checker. On the other hand, maybe it would indeed be better to have `HsTyPat` distinct from `HsType`.... usually, more types are better, no? :) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:3 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 13910, | 13938, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): It's true that there's no counterpart to `Expr`, but perhaps there could be. The problem is that it wouldn't pay its way: the only real usage for the pattern type would be in RULEs. In types, though, patterns come up more often, perhaps tilting the needle enough. Another way of examining this: pattern-matches in terms are elaborately desugared into nested cases. If they weren't, the case for an expression- level pattern type would be stronger. And in types, we don't do this desugaring. On the other hand, there is my sentiment in comment:1. I don't think I'd argue with "Well, that's a good idea, but not worth it since we'll be doing much heavier refactoring soon, anyway." -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:7 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 13910, | 13938, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by goldfire): * owner: (none) => goldfire Comment: After a chat at ICFP, Simon and I agreed that this was worthwhile, but in a very different way than originally proposed: create a new datatype `TypePat`, which would be a ''Core'' type pattern, used in, e.g., `FamInst`. Such a type would have no casts, no type families, and no foralls. Casts can be gotten rid of because the pure unifier (the client of type patterns) never uses them, unless they wrap a variable. And in that case, we can just use a variable with a new, corrected kind, and substitute the new one in for the old one (casting appropriately in the, e.g., type family equation's RHS). This transformation would happen after kind-checking and desugaring. Incidentally, it turns out that the underlying problem that this ticket was originally opened for was fixed by a small fix in the unifier. (The matching substitution must be applied to any cast found in the type pattern.) But that fix might not catch every possible case, while the proposal in this comment should. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:9 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 13910, | 13938, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): While investigating #14270 I found that `SpecConstr` was generating rules with massive coercions, like {{{ RULE "SC:foo" f @(a |> <huge coercion expression>) arg1 arg2 = ... }}} Then I mis-read `Note [Matching in the presence of casts]` in `Unify`, and thought that we simply discarded casts. So I had a go at replacing casts in type patterns with a kind of placeholder `UnivCo`. I now think this is probably all wrong, because I still don't understanding of type patterns involving kind casts. But rather than delete my changes entirely I'll attach them here for future reference. The starting point was a new form of `UnivCoProvenance` to use in type patterns; and a `TypePat` type in `Unify. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 13910, | 13938, 14038 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Conor McBride suggested to Simon today that we could usefully include lots of casts in patterns -- indeed, perhaps we should allow a cast essentially at all points in the pattern grammar. These casts would all be casts by a variable. Then, when matching, if the target has no cast at that spot, the variable is matched with Refl. This approach has the downside of producing big substitutions (with lots of type variables and coercion variables), but it has the upside of likely working. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14119: Refactor type patterns -------------------------------------+------------------------------------- Reporter: goldfire | Owner: goldfire Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: 8.2.1 Resolution: | Keywords: TypeInType Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: 12564, 14270 Related Tickets: | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by simonpj): I'm getting an unexpected pass for `typecheck/should_compile/SplitWD` which is marked as `expect_broken(14119)`. Richard, what's up? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14119#comment:18 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler