#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 ezyang):
Is this because GHC 8.0 (and below) allows an hs-boot file to say data where the implementing module says newtype?
Yep.
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?
Ah, this is very interesting (also, thank you for telling me about the journal paper; I didn't realize you had both an extended mix and a journal copy). What we would like to do is two things: 1. Allow decomposition on newtype givens (currently disallowed because Co_Nth doesn't work on newtypes). If we use the proj-roles here, that should solve the soundness problem. 2. Do decomposition BEFORE unwrapping, so that if we hit `FixEither Age ~R FixEither Int`, we immediately jump to `Age ~R Int`, rather than uselessly infinite loop on the newtype unwrapping. (2) is a bit trickier. Suppose when you have something like this: {{{ type app role T nominal type proj role T phantom newtype T a = MkT a }}} What "roles" should I use in the decomposition here, if I am trying to prove `T Int ~R T Age`? Clearly, the only sound and complete choice is representational. Ignoring proj-roles for a moment, the reason we must flatten before we decompose, even today, is because if we decomposed the constraint above, we would end up with `Int ~N Age` which is unsolvable. So, it seems to me, that eager decomposition will go wrong UNLESS you know the "exact" roles of the newtype (the role computation without any subroling). The subroling doesn't affect soundness but it does affect completeness if your constraint solver doesn't backtrack (which ours does not.) I'm also not sure if just (2) is guaranteed to get us to the point where newtype decomposition will actually apply, but the simple examples I thought of seemed to work (including the one in the paper.) -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/13140#comment:12 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler