GHC: Ticket Query
http://ghc.haskell.org/trac/ghc/query?status=!closed&keywords=~family&order=priority
The Glasgow Haskell Compileren-USGHChttp://ghc.haskell.org/trac/ghc/chrome/site/ghc_logo.png
http://ghc.haskell.org/trac/ghc/query?status=!closed&keywords=~family&order=priority
Trac 1.0.1
http://ghc.haskell.org/trac/ghc/ticket/9587
http://ghc.haskell.org/trac/ghc/ticket/9587#9587: Type checking with type functions introduces many type variables, which remain ambiguous. The code no longer type checks.Sat, 13 Sep 2014 12:35:48 GMToleg<p>
Before the type ambiguity check was introduced, I could write the following code
</p>
<pre class="wiki">{-# 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
</pre><p>
(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.
</p>
<p>
Since then, the type inference has changed and the code no longer type checks:
</p>
<pre class="wiki">
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))
</pre><p>
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.
</p>
Resultshttp://ghc.haskell.org/trac/ghc/ticket/9587#changelog