Changes between Version 2 and Version 3 of Design/NewCoercibleSolver/V2


Ignore:
Timestamp:
Mar 17, 2015 3:13:32 PM (4 years ago)
Author:
goldfire
Comment:

--

Legend:

Unmodified
Added
Removed
Modified
  • Design/NewCoercibleSolver/V2

    v2 v3  
    2121== Solutions ==
    2222
    23 I don't have any. Do you?
     23Simon and I agree that recursive newtypes aren't all that important, except in one case: when we have `newtype N a = ty`, we '''must''' be able to prove `N x ~R ty[a |-> x]`, even in the recursive case. Happily, this is captured by an eager reflexivity check, done after unwrapping. So, that's the plan going forward.
    2424
    2525One very dissatisfying solution is to track role annotations and recursivity and then decide between decomposition and unwrapping based on these flags. For a role-annotated, recursive newtype, we just do our best, for some definition of best.
     
    265265
    266266This should work, but this would require a lot more engineering. The problem is that `AppTy`s can't be decomposed, so it's hard to make the constraints canonical and then usable in substitution.
     267
     268-----------------------------------
     269
     270{{{
     271newtype N1 a = MkN1 a
     272newtype N2 a = MkN2 (N1 a)
     273
     274foo :: N1 a -> N2 a
     275foo = coerce
     276}}}
     277
     278Here, we '''won't''' decompose, because the heads differ. Even though this is similar to a case where we do decompose. Simon says that this means we should prefer unwrapping. I agree.