GitLab

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.

Trac metadata

Trac field	Value
Version	7.8.3
Type	Bug
TypeOfFailure	OtherFailure
Priority	normal
Resolution	Unresolved
Component	Compiler (Type checker)
Test case
Differential revisions
BlockedBy
Related
Blocking
CC
Operating system
Architecture