#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, Richard, others, I'm making progress on this one but before going too far I want to get a green light on my design proposal (points 1-3). I've also bumped into some problems and have a couple of questions. My design proposal is to implement only injectivity of type A (ie. plain injectivity in all arguments). The consequences of this are: 1. A user is allowed to write at most one injectivity condition. 2. That condition must contain only the result type variable on the LHS of `->` and all other type variables on the RHS of `->`. In other words if I declare `type family P a b = r` then I'm only allowed to write `r -> a b` or `r -> b a` injectivity condition. Questions here: a) can I add a restriction that type variables on the RHS must be given in exactly the same order as they were given in the head declaration? This would make the implementation simpler; b) where should this check be done? In the renamer? 3. Once we check 2) we must verify that the type family is indeed injective. Not sure where this should happen? My guess is that during typechecking of a type family equations. Algorithm is outlined [wiki:InjectiveTypeFamilies#Implementationoutline here]. Does the implementation plan outlined so far look sensible? Are there any misconceptions? 4. Once we pass these checks injectivity becomes a binary property, so we can discard injectivity conditions written by the user and replace it with a `Bool`. Richard, when we first spoke about injective type families you suggested that all the magic will go into `isDecomposableTyCon` in `types/TyCon.lhs`. I've added a `Bool` field to `SynTyCon` data constructor of `TyCon` data type and made `isDecomposableTyCon` use that field to tell whether a type family is injective or not. (Checks described in 2 and 3 are not implemented. When a user writes injectivity declaration for a type family I just assume it is correct.) Sadly, this does not work. Here's an example test case: {{{#!hs type family F a = r | r -> a where F Int = Bool F Bool = Int F a = a foo :: F a -> F a foo = id }}} This fails with: {{{ Couldn't match type ‘F a0’ with ‘F a’ NB: ‘F’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: F a -> F a Actual type: F a0 -> F a0 In the ambiguity check for: forall a. F a -> F a To defer the ambiguity check to use sites, enable AllowAmbiguousTypes In the type signature for ‘foo’: foo :: F a -> F a }}} I added traces to verify that `isDecomposableTyCon` is called for `F` type family and it correctly returns `True`. Out of curiosity I turned on `AllowAmbiguousTypes` and added a definition like this: {{{ bar :: Int -> Int bar = foo }}} That failed with: {{{ Couldn't match type ‘F a0’ with ‘Int’ The type variable ‘a0’ is ambiguous Expected type: Int -> Int Actual type: F a0 -> F a0 In the expression: foo In an equation for ‘bar’: bar = foo }}} I imagine that getting this one to work definitely requires more changes than just `isDecomposableTyCon`. Then again GHC can already deal with some cases of injectivity: {{{#!hs type family F a = r | r -> a where F Int = Int F Bool = Bool F a = a foo :: F a -> F a foo = id bar :: Int -> Int bar = foo }}} That works perfectly fine in GHC 7.8. I tried to analyse what's going on with `-ddump-tc-trace` but the dumps are 600-1000 lines long. Of course the source code itself is even longer, so I'd appreciate any directions where should I start looking. One final question. Assuming that `SynTyCon` really should have a new field, I believe this field should be stored in interface files. After all we want injectivity information to propagate from one module to another. Now I wonder how this interacts with open type families. I understand that these are typechecked progressively as we find more equations. I haven't looked at the implementation but my intuition from reading GHC papers is that in a given module we import open type family equations from other modules, collect equations from current module and proceed with type checking of an open type family. Is that intuition correct? If so then I believe that checking of injectivity (point 3 of my outline) should be done during this stage (I believe it would be best to combine it with checking equation overlapping). -- Ticket URL: http://ghc.haskell.org/trac/ghc/ticket/6018#comment:73 GHC http://www.haskell.org/ghc/ The Glasgow Haskell Compiler