Opened 6 years ago

Closed 5 years ago

#3500 closed bug (fixed)

Type functions and recursive dictionaries

Reported by: simonpj Owned by:
Priority: normal Milestone: 7.0.1
Component: Compiler Version: 6.10.4
Keywords: Cc: stefan@…
Operating System: Unknown/Multiple Architecture: Unknown/Multiple
Type of failure: Compile-time crash Test Case: typecheck/should_run/T3500a,b
Blocked By: Blocking:
Related Tickets: Differential Revisions:

Description

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.

Change History (5)

comment:1 Changed 6 years ago by simonpj

You are trying to do something quite delicate here.

The whole idea of solving constraints in a co-inductive way (building a recursive group of dictionary definitions) relies on spotting something we've seen before to "tie the knot". To date, the main application I knew for this fairly exotic idea was described in the SYB3 paper [1]. So I'm curious about your application (and that of anyone else) that relies on this recursive-dictionary-solving mechanism.

Returning to your problem, this "loop spotting" mechanism is rather syntactic at the moment, whereas your application needs something more refined, involving equality modulo type function reductions. Alas, the constraint solving machinery for type classes and for type functions is not properly integrated. I'm amazed it works as well as it does, actually.

We [Manuel, Dimitrios, and I] are (slowly, slowly) working on a complete rewrite of GHC's constraint-solving mechanism. I'm pretty sure that it'll solve this problem among many others. But don't hold your breath. It'll be months not weeks. But not years!

comment:2 Changed 6 years ago by igloo

  • Milestone set to 6.14.1

comment:3 Changed 5 years ago by Saizan

  • Type of failure set to None/Unknown

found another case of this, i think, using ghc-6.12.3:

{-# LANGUAGE TypeFamilies, FlexibleContexts, UndecidableInstances #-}

newtype Mu f = Mu (f (Mu f)) 
     
type family Id m
type instance Id m = m

instance Show (Id (f (Mu f))) => Show (Mu f) where
    show (Mu f) = show f


showMu :: Mu (Either ()) -> String
showMu = show

loading the above code makes ghc loop, it works fine if we remove Id instead. this is a boiled down testcase, the motivating code is from [1] where it seems impossible to write a Show instance for Fix.

[1] http://blog.sigfpe.com/2010/08/constraining-types-with-regular.html

comment:4 Changed 5 years ago by Saizan

  • Type of failure changed from None/Unknown to Compile-time crash

comment:5 Changed 5 years ago by simonpj

  • Resolution set to fixed
  • Status changed from new to closed
  • Test Case set to typecheck/should_run/T3500a,b

These examples work fine with the new typechecker, which will be in GHC 7.0. I'll add them as regression tests though! Thanks.

Simon

Note: See TracTickets for help on using tickets.