#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 jstolarek): Replying to [comment:103 jberryman]:
I've only had use for better type inference with (conceptually) closed, recursive type families Calling type families from an injective type family will not be allowed (including recursion). The reason is that I don't see a way of verifying injectivity when type families are involved.
What I think I want is something like proposal C from the wiki At the moment I am implementing proposals A and B. C is something to think about in the future, as it is not trivial.
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. Yes, I suppose that focus of the wiki discussion is a bit off. I think we could infer injectivity of type A for closed type families. But I don't think we should try to infer injectivity of type B because the algorithm is exponential - see [comment:64 comment 64]. That's the major reason for doing this. (Numbers in that comment were computed for type C injectivity, but type B is also exponential.)
{{{#!hs -- | The algebraic normal form 'Exponent' @abc@ distributed over the single -- base variable @x@. type family abc :=>-> x -- | x¹ = x type instance () :=>-> x = x -- | x⁽ᵃᵇ⁾ = (xᵇ)ᵃ type instance (a,bs) :=>-> x = a -> bs :=>-> x }}} I don't think `:=>->` type family is injective: both `() :=>-> (Int -> Int)` and `(Int,()) :=>-> Int` reduce to `Int -> Int`. -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:104 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler