Type functions and recursive dictionaries
Stefan Holdermans reports: I've spotted a hopefully small but for us quite annoying bug in GHC's type checker: it loops when overloading resolving involves a circular constraint graph containing type-family applications.
The following program demonstrates the problem:
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE TypeFamilies #-}
type family F a :: *
type instance F Int = (Int, ())
class C a
instance C ()
instance (C (F a), C b) => C (a, b)
f :: C (F a) => a -> Int
f _ = 2
main :: IO ()
main = print (f (3 :: Int))
My guess is that the loop is caused by the constraint C (F Int)
that
arises from the use of f in main:
C (F Int) = C (Int, ()) <= C (F Int)
Indeed, overloading can be resolved successfully by "black-holing" the initial constraint, but it seems like the type checker refuses to do so.
Can you confirm my findings?
Since this problem arises in a piece of very mission-critical code, I would be pleased to learn about any workarounds.
Trac metadata
Trac field | Value |
---|---|
Version | 6.10.4 |
Type | Bug |
TypeOfFailure | OtherFailure |
Priority | normal |
Resolution | Unresolved |
Component | Compiler |
Test case | |
Differential revisions | |
BlockedBy | |
Related | |
Blocking | |
CC | stefan@cs.uu.nl |
Operating system | |
Architecture |