Opened 5 years ago

Last modified 17 months ago

#9587 new bug

Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.

Reported by: oleg Owned by:
Priority: normal Milestone:
Component: Compiler (Type checker) Version: 7.8.3
Keywords: TypeFamilies, ambiguity check Cc:
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: GHC rejects valid program Test Case:
Blocked By: Blocking:
Related Tickets: #9607 Differential Rev(s):
Wiki Page:

Description

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.

Change History (13)

comment:1 Changed 5 years ago by simonpj

Just to be clear, are you saying that -XAllowAmbiguousTypes does not suppress the error? (Which it claims to do.)

Simon

comment:2 Changed 5 years ago 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.

comment:3 Changed 5 years ago 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

comment:4 Changed 5 years ago 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.

comment:5 Changed 5 years ago 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

comment:6 Changed 5 years ago by jstolarek

comment:7 Changed 5 years ago 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?

comment:8 in reply to:  7 Changed 5 years ago by dfeuer

Replying to 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?

comment:9 Changed 4 years ago by jstolarek

Oleg, is Arr injective? If it is then this should by fixed by #6018, which should be merged Real Soon Now.

comment:10 Changed 4 years ago 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.

comment:11 Changed 4 years ago 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.

comment:12 in reply to:  10 Changed 4 years ago by jstolarek

For the record, this code can now be compiled using injective type families:

{-# 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 the actual injectivity annotation on Arr is r repr -> a b and that is not supported yet

comment:13 Changed 17 months ago by RyanGlScott

Keywords: TypeFamilies added; type family removed
Note: See TracTickets for help on using tickets.