#6018: Injective type families -------------------------------------+------------------------------------- Reporter: lunaris | Owner: jstolarek Type: feature | Status: new request | Milestone: 7.10.1 Priority: normal | Version: 7.4.1 Component: Compiler | Keywords: TypeFamilies, Resolution: | Injective Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: | Blocked By: None/Unknown | Related Tickets: #4259 Test Case: | Blocking: | Differential Revisions: Phab:D202 | -------------------------------------+------------------------------------- Comment (by jstolarek): Simon, I'm trying to understand your [comment:76 earlier comment]:

* We are not (at least for now) changing System FC. So the only effect of injectivity is to add extra "Derived" unification constraints, very much like functional dependencies. If we see {{{ [W] F t ~ F s }}} then we don't decopose it. Instead we add {{{ [D] t ~ s }}} That guides inference, but does not produce proof terms. So, no, nothing to do with `isDecomposableTyCon`. Much more like the `try_improvement` code in `TcInteract.doTopReactFunEq`.

First of all, do we ever get a chance of actually seeing `F t ~ F s`? I think this is not canonical and if such constraint ever appears it would be turned into `F t ~ a, F s ~ a`. I'm not sure which of the canonicalization rules in Fig. 21 in OutsideIn paper would be responsible for that conversion because I don't know the meaning of these stylized D, F and T used in the mentioned figure. My guess would be FFLAT[W/G]R rules. Anyway, once we have `F t ~ a, F s ~ a` we could apply my suggested INJFEQFEQ interaction rule to generate `[D] s ~ t`. If my thinking here is right then shouldn't the implementation go into `TcInteract.interactFunEq` (guessing from its name)? I also wonder whether `[W]` is important in your `[W] F t ~ F s` example? I believe this rule is valid for both given and wanted constraints. I don't understand what you mean by "we don't decopose it". What is this "decomposition" that you mention? I believe that the only moment when injectivity interacts with top-level axioms is when we're deducing LHS from RHS. I suspect this might require a new reaction rule, separate from FINST. Are my ideas here correct? -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:90 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler