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

13 Sep 2014

      #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