#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): Yes, it makes sense to put this in `TyCoRep`, so that only some modules gain access to the constructors. I'm not so worried about `Functor` and friends. If this turns out to bite, we can always fix it later. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:2 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tdammers): Turns out there are a few places in the code that exploit `Maybe`'s `Monad` instance (using `do` notation). I'll keep those as `Maybe` for now and see where I end up. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:4 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tdammers): I've been doing some work on this in between other stuff, but haven't gotten very far yet. I have a `MCoercion` type in place (which is trivial), and my first approach was to just naively replace all `Maybe Coercion`s with `MCoercion` and then follow the compiler errors. However, this doesn't work out all that well, because some of those `Maybe`s are actually morally justified as such (i.e., `Nothing` does not not mean "this is a Refl coercion", but it actually means "nothing found" / "failure"). I was going to go through the code and look at all occurrences individually, but haven't gotten around to this yet. If someone wants to take this off me, and do the work for free, I say go ahead, I'm not emotionally invested in this. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:6 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

Hi there. This is Ningning. I am one of the students of GSoC this year under advised by Richard. Find more information about [https://summerofcode.withgoogle.com/projects/#5851493949767680/ my

#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: new Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Comment (by tdammers): Replying to [comment:7 ningning]: proposal].

Thanks to tdammers, I am taking this ticket as my warm-up exercise :).

Great! The code I have so far is on the GHC git repo, in the wip/T14975 branch. Though not strictly necessary for this, you may want to also look into tickets #11735, #14737 and #15019 for context. Let us know if there's anything else you need. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:8 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: patch Priority: normal | Milestone: Component: Compiler | Version: Resolution: | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Phab:D4699 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Ben Gamari ): In [changeset:"9aac442f70b0b58decd56fb52dd4ec2289b03759/ghc" 9aac442/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="9aac442f70b0b58decd56fb52dd4ec2289b03759" Define MCoercion type An attempt on #14975: During compilation, reflexive casts is discarded for computation. Currently in some places we use Maybe coercion as inputs. So if a cast is reflexive it is denoted as Nothing, otherwise Just coercion. This patch defines the type data MCoercion = MRefl | MCo Coercion which is isomorphic to Maybe Coercion but useful in a number of places, and super-helpful documentation. Test Plan: validate Reviewers: bgamari, goldfire, simonpj Reviewed By: goldfire Subscribers: mpickering, rwbarton, thomie, carter GHC Trac Issues: #14975 Differential Revision: https://phabricator.haskell.org/D4699 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:10 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler

#14975: Refactor (Maybe Coercion) -------------------------------------+------------------------------------- Reporter: tdammers | Owner: (none) Type: task | Status: closed Priority: normal | Milestone: 8.6.1 Component: Compiler | Version: Resolution: fixed | Keywords: Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: #11735 | Differential Rev(s): Phab:D4699 Wiki Page: | -------------------------------------+------------------------------------- Comment (by Richard Eisenberg ): In [changeset:"55a3f8552c9dc9b84e204ec6623c698912795347/ghc" 55a3f85/ghc]: {{{ #!CommitTicketReference repository="ghc" revision="55a3f8552c9dc9b84e204ec6623c698912795347" Refactor coercion rule Summary: The patch is an attempt on #15192. It defines a new coercion rule ``` | GRefl Role Type MCoercion ``` which correspondes to the typing rule ``` t1 : k1 ------------------------------------ GRefl r t1 MRefl: t1 ~r t1 t1 : k1 co :: k1 ~ k2 ------------------------------------ GRefl r t1 (MCo co) : t1 ~r t1 |> co ``` MCoercion wraps a coercion, which might be reflexive (MRefl) or not (MCo co). To know more about MCoercion see #14975. We keep Refl ty as a special case for nominal reflexive coercions, naemly, Refl ty :: ty ~n ty. This commit is meant to be a general performance improvement, but there are a few regressions. See #15192, comment:13 for more information. Test Plan: ./validate Reviewers: bgamari, goldfire, simonpj Subscribers: rwbarton, thomie, carter GHC Trac Issues: #15192 Differential Revision: https://phabricator.haskell.org/D4747 }}} -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/14975#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler