[GHC] #9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Operating System: Keywords: type family, | Unknown/Multiple ambiguity check | Type of failure: GHC Architecture: Unknown/Multiple | rejects valid program Difficulty: Unknown | Test Case: Blocked By: | Blocking: Related Tickets: | Differential Revisions: -------------------------------------+------------------------------------- Before the type ambiguity check was introduced, I could write the following code {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} -- {-# LANGUAGE AllowAmbiguousTypes #-} module T where type family Arr (repr :: * -> *) (a :: *) (b :: *) :: * class ESymantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (Arr repr a b) app :: repr (Arr repr a b) -> repr a -> repr b {- te4 :: (Arr repr (Arr repr Int Int) (Arr repr Int Int) ~ Arr repr (Arr repr Int Int) (Arr repr Int b), ESymantics repr) => repr b -} te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x)))) in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) -- t = lam (\f -> f `app` int 0) newtype R a = R{unR :: a} type instance Arr R a b = a -> b instance ESymantics R where int = R add (R x) (R y) = R $ x + y lam f = R $ unR . f . R app (R f) (R x) = R $ f x tR = unR te4 }}} (This is a simple code abstracted from a longer code that for sure worked in 2010: I showed it in a SSGIP lecture at Oxford.) The inferred type of te4 is shown in comments. The type is not ideal but the best what can be done under circumstances. In tR, repr is instantiated to R and the type function Arr can finally be applied and the equality constraint resolved. Since then, the type inference has changed and the code no longer type checks: {{{ Could not deduce (Arr repr (Arr repr a0 b0) (Arr repr a2 b0) ~ Arr repr (Arr repr a b) (Arr repr a4 b)) from the context (ESymantics repr, Arr repr a4 a3 ~ Arr repr a b, Arr repr a3 a ~ Arr repr a b) bound by the inferred type for ‘c3’: (ESymantics repr, Arr repr a4 a3 ~ Arr repr a b, Arr repr a3 a ~ Arr repr a b) => repr (Arr repr (Arr repr a b) (Arr repr a4 b)) }}} What is worse, there does not appear to be *any* way to get the code to type check. No amount of type annotations helps. The code has to be dramatically re-written, or just given up. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): Just to be clear, are you saying that `-XAllowAmbiguousTypes` does not suppress the error? (Which it claims to do.) Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:1> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by oleg): Correct: uncommenting the line {-# LANGUAGE AllowAmbiguousTypes #-} does not change the behavior of the type checker for the code in question. And looking at the error message, I didn't think it would. The program is plainly rejected and I don't see what I can possibly do to get it accepted again. I have tried many annotations and small re-writings, to no avail. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:2> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I've tried this with GHC 7.6 and 7.4 as well as 7.8.3. When compiling the code you give above, all of them say {{{ T9587.hs:26:11: Could not deduce (Arr repr (Arr repr a4 a3) (Arr repr a4 b) ~ Arr repr (Arr repr a2 a1) (Arr repr a2 b0)) from the context (ESymantics repr, Arr repr a3 a ~ Arr repr a4 a3, Arr repr a b ~ Arr repr a4 a3) bound by the inferred type for `c3': (ESymantics repr, Arr repr a3 a ~ Arr repr a4 a3, Arr repr a b ~ Arr repr a4 a3) => repr (Arr repr (Arr repr a4 a3) (Arr repr a4 b)) at T9587.hs:26:11-68 NB: `Arr' is a type function, and may not be injective Expected type: repr (Arr repr (Arr repr a3 a) (Arr repr a3 b)) Actual type: repr (Arr repr (Arr repr a2 a1) (Arr repr a2 b0)) When checking that `c3' has the inferred type `forall (repr1 :: * -> *) b1 a4 a5 a6. (ESymantics repr1, Arr repr1 a5 a4 ~ Arr repr1 a6 a5, Arr repr1 a4 b1 ~ Arr repr1 a6 a5) => repr1 (Arr repr1 (Arr repr1 a6 a5) (Arr repr1 a6 b1))' Probable cause: the inferred type is ambiguous In the expression: let c3 = lam (\ f -> lam (\ x -> ...)) in (c3 `app` (lam (\ x -> x `add` int 14))) `app` (int 0) }}} So are you saying that something has changed? If so, what? Thanks Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:3> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by oleg): I have checked with GHC 7.4.1 as well. It does report the error you quote. And yet the code did work back in 2010 at least, and inferred the type mentioned in my original Trac submission. The change in type inference must have happened sometime around GHC 7.2->7.4. It did break the code, some of which I had to rewrite (and the rest just abandoned). Let's look at the error message closely: {{{ Could not deduce (Arr repr (Arr repr a4 a3) (Arr repr a4 b) ~ Arr repr (Arr repr a2 a1) (Arr repr a2 b0)) from the context (ESymantics repr, Arr repr a3 a ~ Arr repr a4 a3, Arr repr a b ~ Arr repr a4 a3) }}} Since Arr is a function, then choosing a2~a4, a1~a3, b0~b will certainly satisfy the offending constraint. Since the type variables a2, a1, b0 are not mentioned anywhere else, there is no risk of conflicts. I think that's what GHC 7.0 (or 7.2) must have done. True, we must have lost principality. But the principality was lost already in Haskell98, so there is no use to worry about it now. I cannot help but notice the irony: type functions were introduced in 2005 as a `functional' alternative to functional dependencies. Programming with functional dependencies was viewed as logic programming. We are functional programmers, we should program with functions. the slogan went. Alas, when it comes to inference, we need to know what can we infer about t1 and t2 from Fn t1 ~ Fn t2. So, we do have to think relationally rather than functionally -- it is inherent. We have not escaped from the relational view -- merely made it harder to see, which is not always an advantage. BTW, adding the declaration for injective type families may be not enough. For example, consider our Arr repr t1 t2. It could be that Arr repr t1 t2 is injective only for specific repr. We intend to use our example only with such repr. But Arr repr t1 t2 may be usable for different repr, which do not correspond to injective Arr repr. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:4> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by simonpj): I tried with 7.0. Yes, if you omit the type signature for `te4`, GHC 7.0 will infer the one you give. But if you write in that type signature, 7.0 will reject the program with the same error, which is hardly satisfactory. No, GHC 7.0 did not "guess" some type-variable equalities that would solve the constraints. I have absolutely no idea how to do this in general, and GHC has never attempted to do so. It's just that 7.0 allowed you to infer a type that, if you wrote it as the signature, would be rejected. GHC 7.4 etc don't do that, which on the whole is a good thing. While I could reverse that decision, it doesn't seem like the right way to solve the problem. The right way is to get GHC to make right instantiations, along the lines you mention. How can we do that? Usually by supplying some type signatures. I don't understand the code well enough, but can you do this? * write the type sig for `te4`, using a `forall` so that the type variables scope over the body, * give some type signatures in the body so that the type variable equalities you want are forced Alternatively, do you have any other suggestions for how to guide GHC to make the right choices during inference? Especially if injectivity won't do it. Mind you, injectivity might do it if you used an auxiliary family for the particular `repr` you care about. Eg {{{ type family Arr r a b :: * type instance Arr MyRepr a b = MyArr a b -- Arr is not injective type family MyArr a b :: * | result -> a b -- MyArr is injective }}} Might that work? I'm sure you will have other creative ideas. Simon -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:5> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: #9607 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Changes (by jstolarek): * related: => #9607 -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:6> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: #9607 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by oleg): I have played with giving type annotations for quite a long time, without success. Let's take the same example: {{{ {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE AllowAmbiguousTypes #-} module T where type family Arr (repr :: * -> *) (a :: *) (b :: *) :: * class ESymantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (Arr repr a b) app :: repr (Arr repr a b) -> repr a -> repr b {- te4 :: (Arr repr (Arr repr Int Int) (Arr repr Int Int) ~ Arr repr (Arr repr Int Int) (Arr repr Int b), ESymantics repr) => repr b -} te4 :: forall repr. ESymantics repr => repr Int te4 = let c3 :: forall a. repr (Arr repr (Arr repr a a) (Arr repr a a)) c3 = lam (\f -> lam (\x -> f `app` ((f :: repr (Arr repr a a)) `app` ((f `app` (x::repr a) :: repr a) :: repr a) ) :: repr a) :: repr (Arr repr a a)) in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) }}} Here I have annotated everything of importance, I think. All binders are annotated and all applications are annotated. We really don't want to do it in real programs. And yet the type checker is unhappy: {{{ Could not deduce (Arr repr a0 a ~ Arr repr a a) from the context (ESymantics repr) bound by the type signature for te4 :: ESymantics repr => repr Int at /tmp/u.hs:(26,8)-(27,34) NB: ‘Arr’ is a type function, and may not be injective The type variable ‘a0’ is ambiguous Expected type: repr (Arr repr a0 a) Actual type: repr (Arr repr a a) Relevant bindings include x :: repr a (bound at /tmp/u.hs:30:29) f :: repr (Arr repr a a) (bound at /tmp/u.hs:30:18) c3 :: repr (Arr repr (Arr repr a a) (Arr repr a a)) (bound at /tmp/u.hs:30:7) te4 :: repr Int (bound at /tmp/u.hs:28:1) In the first argument of ‘app’, namely ‘f’ In the expression: f `app` ((f :: repr (Arr repr a a)) `app` ((f `app` (x :: repr a) :: repr a) :: repr a)) :: repr a }}} We see all bindings in scope have the right type; we don't seem to have any more places to add a type annotation that change things. I wonder what wrong could happen if we just assume injectivity in such cases. Let's take an example of type family Add to add two type-level numerals (represented in unary, for example). Clearly Add is not injective. Therefore, from the constraint Add x y ~ Add 1 2 we cannot infer that x ~ 1 and y ~ 2. Although x~1, y~2 do satisfy the constraint, there are other satisfactory pairs. Suppose however that x and y are not mentioned anywhere else in the type or the type environment. Then setting them to x~1 and y~2 will not lead to any contradiction. Hence my suggestion: if type checking gets stuck on trying to deduce the equality constraint LHS ~ RHS, try to solve this constraint using unification (that is, assume injectivity of all type functions used in the constraint). Unification will give a set of equalities x1 ~ y1, x2 ~ y2, etc. Of these equalities, accept only those that involve a type variable that appears only once in the inferred equalities and does not appear anywhere else (in types or the type environment). Repeat the type checking using the accepted equalities. What do you think? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:7> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler | Version: 7.8.3 (Type checker) | Keywords: type family, Resolution: | ambiguity check Operating System: | Architecture: Unknown/Multiple Unknown/Multiple | Difficulty: Unknown Type of failure: GHC | Blocked By: rejects valid program | Related Tickets: #9607 Test Case: | Blocking: | Differential Revisions: | -------------------------------------+------------------------------------- Comment (by dfeuer): Replying to [comment:7 oleg]:
I have played with giving type annotations for quite a long time, without success. .... I wonder what wrong could happen if we just assume injectivity in such cases.
If I understand simonpj correctly, he would like to make sure it is possible to give explicit signatures ''first'', even if those would be nasty to write and/or read, and only add inference rules for such afterwards. This sounds reasonable to me, but I'm no expert. Maybe this will finally push him to implement the explicit type applications he's mentioned in the past? -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:8> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: type Resolution: | family, ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jstolarek): Oleg, is `Arr` injective? If it is then this should by fixed by #6018, which should be merged Real Soon Now. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:9> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: type Resolution: | family, ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by oleg): Well, Arr is a function of three arguments. For a particular choice R for the first argument, Arr R is a->b and hence injective, but one may well define Arr R' a b = String, for example. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:10> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: type Resolution: | family, ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jstolarek):
one may well define Arr R' a b = String
But the question is whether `Arr R' a b = String` is an acceptable definition? If yes, then of course injectivity is not a solution. -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:11> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: type Resolution: | family, ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Revisions: -------------------------------------+------------------------------------- Comment (by jstolarek): For the record, this code can now be compiled using injective type families: {{{#!hs {-# LANGUAGE NoMonomorphismRestriction #-} {-# LANGUAGE TypeFamilies #-} {-# LANGUAGE KindSignatures #-} {-# LANGUAGE ScopedTypeVariables #-} module T9587 where type family Arr (repr :: * -> *) (a :: *) (b :: *) = (r :: *) | r -> repr a b class ESymantics repr where int :: Int -> repr Int add :: repr Int -> repr Int -> repr Int lam :: (repr a -> repr b) -> repr (Arr repr a b) app :: repr (Arr repr a b) -> repr a -> repr b te4 = let c3 = lam (\f -> lam (\x -> f `app` (f `app` (f `app` x)))) in (c3 `app` (lam (\x -> x `add` int 14))) `app` (int 0) }}} Not sure if that addresses the original problem because: a) `Arr` might not be injective at all b) if I understand correctly [comment:10 comment 10] the actual injectivity annotation on `Arr` is `r repr -> a b` and that is not supported yet -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:12> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks. -------------------------------------+------------------------------------- Reporter: oleg | Owner: (none) Type: bug | Status: new Priority: normal | Milestone: Component: Compiler (Type | Version: 7.8.3 checker) | Keywords: TypeFamilies, Resolution: | ambiguity check Operating System: Unknown/Multiple | Architecture: Type of failure: GHC rejects | Unknown/Multiple valid program | Test Case: Blocked By: | Blocking: Related Tickets: #9607 | Differential Rev(s): Wiki Page: | -------------------------------------+------------------------------------- Changes (by RyanGlScott): * keywords: type family, ambiguity check => TypeFamilies, ambiguity check -- Ticket URL: <http://ghc.haskell.org/trac/ghc/ticket/9587#comment:13> GHC <http://www.haskell.org/ghc/> The Glasgow Haskell Compiler
participants (1)
-
GHC