[GHC] #14119: Refactor type patterns

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
11 messages Options
Reply | Threaded
Open this post in threaded view
|

[GHC] #14119: Refactor type patterns

GHC - devs mailing list
#14119: Refactor type patterns
-------------------------------------+-------------------------------------
           Reporter:  goldfire       |             Owner:  (none)
               Type:  task           |            Status:  new
           Priority:  normal         |         Milestone:
          Component:  Compiler       |           Version:  8.2.1
           Keywords:  TypeInType     |  Operating System:  Unknown/Multiple
       Architecture:                 |   Type of failure:  None/Unknown
  Unknown/Multiple                   |
          Test Case:                 |        Blocked By:
           Blocking:  12564, 14038   |   Related Tickets:
Differential Rev(s):                 |         Wiki Page:
-------------------------------------+-------------------------------------
 Type patterns are used in instance heads: class instances, type instances,
 and data/newtype instances. These type patterns differ from ordinary types
 in several ways:

  * They must never mention a `forall`.
  * They must never mention a context. (The context in a class instance
 head is a different part of the instance construct.)
  * They must never mention a type family.

 Types that appear as arguments on the LHS of a RULE should also be type
 patterns.

 Type patterns are used in GHC differently than types as well: we should
 match only against patterns, never ordinary types.

 I thus propose that a new datatype within GHC to store type patterns. I'll
 call it `TyPat` here, but perhaps a longer name is better. The matcher (in
 the `Unify` module) would then take a `TyPat` parameter, making clear
 which type is the template and which is the concrete instantiation.

 We could have a new algorithm to typecheck/desugar source syntax into
 patterns. This new algorithm could accommodate issues like those mentioned
 in comment:6:ticket:14038. It could also avoid ever putting a type family
 in a kind parameter, which would fix #12564. Separating out checking type
 patterns from proper types could also improve GADT pattern matching in
 types, which is currently more like "wobbly types" than OutsideIn.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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:                    |
-------------------------------------+-------------------------------------
Changes (by RyanGlScott):

 * cc: RyanGlScott (added)


Comment:

 Silly question: are you proposing that we introduce a counterpart for
 `HsType` (from user syntax) for type patterns? A counterpart to `Type`
 (from Core) for type patterns? Both?

 If a counterpart for `HsType` is in the works, I think it would be a good
 idea for another reason. Currently, there are some niceties that term-
 level patterns provide which aren't available for type-level patterns,
 such as as-patterns (e.g., `x@(Just y)`). If we had a separate data
 type(s) for type patterns, it would be much easier to add support for this
 feature, since we would have a way to rule out the use of as-patterns in
 non-pattern types.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119#comment:2>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 simonpj):

 I'm not convinced.

 You are proposing a counterpart to `Type`. But there is no counterpart to
 `Expr` in Core.  Indeed, in RULEs the patterns are indeed `Expr`s.  And
 casts in terms can indeed mess things up a bit; see `Rules.match`.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119#comment:6>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 simonpj):

 > 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."

 Yes, I think we have enough else to do.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119#comment:8>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 Simon Peyton Jones <simonpj@…>):

 In [changeset:"9218ea60faa744803fb41066aedd1da8f1bd9185/ghc"
 9218ea60/ghc]:
 {{{
 #!CommitTicketReference repository="ghc"
 revision="9218ea60faa744803fb41066aedd1da8f1bd9185"
 Interim fix for a nasty type-matching bug

 The type matcher in types/Unify.hs was producing a substitution
 that had variables from the template in its range.  Yikes!

 This patch, documented in Note [Matching in the presence of casts],
 is an interm fix.  Richard and I don't like it much, and are
 pondering a better solution (Trac #14119).

 All this came up in investigating Trac #13910. Alas this patch
 doesn't fix #13910, which still has ASSERT failures, so I have
 not yet added a test.  But the patch does fix a definite bug.
 }}}

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119#comment:10>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets
Reply | Threaded
Open this post in threaded view
|

Re: [GHC] #14119: Refactor type patterns

GHC - devs mailing list
In reply to this post by GHC - devs mailing list
#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 simonpj):

 * Attachment "type-pats" added.

 Half-baked patch for type patterns

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/14119>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler

_______________________________________________
ghc-tickets mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-tickets