[GHC] #6018: Injective type families

[GHC]

#6018: Injective type families
-------------------------------------+-------------------------------------
        Reporter:  lunaris           |                   Owner:  jstolarek
            Type:  feature request   |                  Status:  new
        Priority:  normal            |               Milestone:  7.12.1
       Component:  Compiler          |                 Version:  7.4.1
      Resolution:                    |                Keywords:
Operating System:  Unknown/Multiple  |  TypeFamilies, Injective
 Type of failure:  None/Unknown      |            Architecture:
      Blocked By:                    |  Unknown/Multiple
 Related Tickets:  #4259             |               Test Case:
                                     |                Blocking:
                                     |  Differential Revisions:  Phab:D202
-------------------------------------+-------------------------------------

Comment (by jberryman):

 I'm very late to the discussion, so this is probably not helpful at all,
 but I wanted to mention my interest. I've only had use for better type
 inference with (conceptually) closed, recursive type families. What I
 think I want is something like proposal C from the wiki, or the head-
 injectivity proposal where "possibly-partial information about the result
 might allow us to deduce possibly-partial information about the
 arguments."

 And as a naive user I want injectivity to be inferred for closed type
 families, and don't find the arguments against it in the wiki convincing.
 Intuitively there doesn't seem to be much difference between the level of
 logic required to infer things about types with closed type synonym
 families, vs the sort of inference the typechecker does elsewhere (again,
 as a naive user who doesn't care about the trickiness of implementing such
 a scheme). My impression is that this is what many people assumed would be
 the point of closed type families; for what I've had in mind closed type
 families make only a cosmetic improvement.

 Anyway most of my interest came from my work on
 https://github.com/jberryman/shapely-data which embarrassingly seems to
 dependent quite a lot on #1241, so it (and below) needs GHC 7.6. You can
 ignore the example that follows or consider it if it's helpful:

 {{{#!hs
 {-# LANGUAGE TypeOperators #-}
 {-# LANGUAGE TypeFamilies #-}
 {-# LANGUAGE MultiParamTypeClasses #-}
 {-# LANGUAGE FlexibleInstances #-}
 {-# LANGUAGE FlexibleContexts #-}
 {-# LANGUAGE UndecidableInstances #-}  -- for nested Type family: Reversed
 (Tail t) :> Head t
 {-# LANGUAGE FunctionalDependencies #-}

 -- | A class for the exponent laws with the 'Normal' form @abc@ in the
 exponent
 -- place. See the instance documentation for concrete types and examples.
 class Exponent abc where
     fanin :: (abc :=>-> x) -> (abc -> x)
     unfanin :: (abc -> x) -> (abc :=>-> x)

 -- | The algebraic normal form 'Exponent' @abc@ distributed over the
 single
 -- base variable @x at .
 type family abc :=>-> x
 -- | x¹ = x
 type instance () :=>-> x = x
 -- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ
 type instance (a,bs) :=>-> x = a -> bs :=>-> x

 instance Exponent () where
     fanin = const
     unfanin f = f ()

 instance (Exponent bs)=> Exponent (a,bs) where
     fanin f = uncurry (fanin . f)
     unfanin f = unfanin . curry f


 class Homogeneous a as | as -> a where
     -- An n-ary @codiag at .
     genericRepeat :: a -> as

 instance Homogeneous a () where
     genericRepeat _ = ()

 instance (Homogeneous a as)=> Homogeneous a (a,as) where
     genericRepeat a = (a,genericRepeat a)
 }}}

 So the following two type-check fine:

 {{{#!hs
 a = (3 ==) $ (\(x,(y,(z,())))-> x+y+z) $ genericRepeat 1
 b = (3 ==) $ fanin (\x y z-> x+y+z) (genericRepeat 1 ::
 (Int,(Int,(Int,()))))
 }}}

 But this doesn't:

 {{{#!hs
 c = (3 ==) $ fanin (\x y z-> x+y+z) $ genericRepeat 1
 }}}

 ...failing with

 {{{
     Couldn't match expected type `a1 -> a1 -> a1 -> a1'
                 with actual type `abc0 :=>-> a0'
     The type variables `a0', `abc0', `a1' are ambiguous
     Possible fix: add a type signature that fixes these type variable(s)
     The lambda expression `\ x y z -> x + y + z' has three arguments,
     but its type `abc0 :=>-> a0' has none
     In the first argument of `fanin', namely `(\ x y z -> x + y + z)'
     In the expression: fanin (\ x y z -> x + y + z)
 }}}

 That library is probably going in the garbage bin at this point, but in
 general this is the sort of thing I think I'd like to be able to do with
 type families eventually. And I haven't gotten to dig into y'all's
 singletons work yet, so it might be that that's the sort of thing I'm
 looking for and my use of type families and classes in shapely-data is
 ill-considered.

 Thanks for your work on this!

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