[GHC] #9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.

[GHC]

#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