#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): If we're not aiming to get this into 7.10 then I guess there's no rush. Replying to [comment:93 simonpj]:

All I plan to do is add a rule along the lines of {{{ [W] F ty1 ~ rhs [W] F ty2 ~ rhs ===> add a new constraint (if F is injective) [D] ty1 ~ ty2 }}} very like functional dependencies for type classes. Yes, that's what I meant with my INJFEQFEQ interaction rule in [comment:89 comment 89]: {{{ INJFEQFEQ interact[l] (F \vec{Xi_1} ~ Xi, F \vec{Xi_2} ~ Xi) = (F \vec{Xi_1} ~ Xi, \vec{ Xi_1 ~ Xi_2 }) }}} Sorry if that wasn't clear. (Now I realized that checking whether `F` is injective might be consider a reaction with top-level axiom and thus this should be a reaction rule.)

But it seems to me there should be one more rule. Consider this example: {{{#!hs type family F a = r | r -> a where F Char = Bool F Bool = Char F a = a idChar :: (F a ~ Bool) => a -> Char idChar a = a }}} Here we have constraint `F a ~ Bool`. Knowing that `F` is injective and it's RHS is `Bool` we want to deduce that `a` must be `Char`. This one seems more difficult because we have to look through all the equations. My guess would be that when we have to do this before constraint solving (in `TcM` monad?). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:94 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler