[GHC] #6018: Injective type families

[GHC]

#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):

 Replying to [comment:79 goldfire]:
 > I'm ambivalent on this design decision (that the variables have to be in
 the same order in the annotation). I suppose it simplifies the
 implementation.

 I guess my argument about simpler implementation is not that important. I
 mean the code is quite simple in both cases. It's more like a choice
 between linear and quadratic algorithm. I'd went for linear, even if it
 adds an extra restriction on the user code.

 > Yes, Simon's comment above is correct -- I was just wrong about the
 `isDecomposableTyCon` thing.

 OK. Reverting :-)

 > What works perfectly fine? Not the code you wrote above, because it
 contains a not-currently-parsed injectivity annotation. I tried it without
 the injectivity annotation, and it does indeed work.

 Yes, that's what I meant.

 > But not because of injectivity, at all: it's because GHC is clever
 enough to figure out that `F` is just an identity function

 Right. Still, I wondering how this works. I mean there are probably no
 special cases in the typechecker that try to guess whether a type family
 is an identity function?

 > Fair warning: 1000 lines of `-ddump-tc-trace` isn't long at all! :)

 I imagine, given that my source file was 8 lines of code. Still, it's a
 bit steep learning curve.

 Replying to [comment:80 goldfire]:
 > Under the singletons work, we gave a different kind to non-injective
 functions

 Ah, right.

 Replying to [wiki:InjectiveTypeFamilies wiki comments]:
 > I believe this would also have to check that all variables mentioned in
 the LHS are mentioned in the RHS. Or, following along with Simon's idea in
 comment:76:ticket:6018, those variables that appear in the injectivity
 annotation must be mentioned in the RHS.

 I haven't thought about that. I believe you're right.

 > We have to be careful with the word overlap here. I think we want
 "overlaps" to be "is subsumed by".

 I don't see the difference between "overlaps" and "is subsumed by". :-(

 Now, in 4c I wrote:

 > if unification [of the RHSs] succeeds and there are type variables
 involved we substitute unified type variables on the LHS and check whether
 this LHS overlaps with any of the previous equations. If it does we
 proceed to the next equation

 You replied with this:

 > you want to know of the equation at hand is reachable, given the LHS
 substitution. Even if it is reachable, the (substituted) LHS may coincide
 with the LHS of the earlier equation whose RHS unified with the current
 RHS.

 I don't see the difference between your version and mine.

 > Even subtler, it's possible that certain values for type variables are
 excluded if the current LHS is reachable (for example, some variable a
 couldn't be Int, because if a were Int, then a previous equation would
 have triggered). Perhaps these exclusions can also be taken into account.

 Hm... can you give an example where this would be useful?

 > '''RAE:''' But it seems that, under this treatment, any self-recursion
 would automatically lead to a conclusion of "not injective", just like any
 other use of a type family. For example:
 >
 > {{{#!hs
 > type family IdNat n where
 >   IdNat Z = Z
 >   IdNat (S n) = S (IdNat n)
 > }}}
 >
 > `IdNat` is injective. But, following the algorithm above, GHC would see
 the recursive use of `IdNat`, not know whether `IdNat` is injective, and
 then give up, concluding "not injective". Is there a case where the
 special treatment of self-recursion leads to a conclusion of "injective"?
 '''End RAE'''

 This example is just like my `NatToMaybe`. My idea here was that RHSs of
 these two equations won't unify - first returns `Z`, second returns `S
 something`. These are distinct constructors that have no chance of being
 unified. (I assumed that we are able to detect that.) There are no calls
 to type families other than self-recursion and so we can declare `IdNat`
 to be injective. I admit I am not 100% certain that allowing self-
 recursion is safe. It's just that I was unable to come up with an example
 that would show that my algorithm: a:) declares injective function to be
 non-injective; b) declares a non-injective function to be injective.

--
Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/6018#comment:82>
GHC <http://www.haskell.org/ghc/>
The Glasgow Haskell Compiler