#13140: Handle subtyping relation for roles in Backpack -------------------------------------+------------------------------------- Reporter: ezyang | Owner: ezyang Type: feature request | Status: patch Priority: normal | Milestone: 8.4.1 Component: Compiler (Type | Version: 8.1 checker) | Keywords: backpack hs- Resolution: | boot Operating System: Unknown/Multiple | Architecture: | Unknown/Multiple Type of failure: None/Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Rev(s): Phab:D3123 Wiki Page: | -------------------------------------+------------------------------------- Comment (by goldfire): I like comment:10. I had forgotten that abstract types were not injective w.r.t. representational equality. Is this because GHC 8.0 (and below) allows an hs-boot file to say `data` where the implementing module says `newtype`? I can't think of another reason. In any case, this is a happy ending to your story. As for the app-roles vs. proj-roles: very interesting. Currently, the solver runs into a problem when proving, say, `N a ~R N b`, where `N` is a newtype whose constructor is in scope: should we unwrap the newtype? Or use decomposition? (Note that this is somewhat the converse problem to the discussion above. Here we're trying to ''prove'' `N a ~R N b`; previous discussion assumed `N a ~R N b` and was trying to learn about `a` and `b`.) I forget exactly what happens here -- it's all in the [http://cs.brynmawr.edu/~rae/papers/2016/coercible-jfp/coercible-jfp.pdf paper]. But I do remember that the resolution was dissatisfyingly incomplete in the case of recursive newtypes. Perhaps Edward's idea in comment:10 -- separate out two sets of roles -- provides a better way forward. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:11 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler