[Haskell-cafe] Resolving overloading loops for circular constraint graph

2009-09-09 Thread Stefan Holdermans 

Manuel, Simon,

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 (also attached) 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?

I'm not sure whether this is a known defect. If it isn't, I'd be more  
than happy to issue a report.


Since this problem arises in a piece of very mission-critical code, I  
would be pleased to learn about any workarounds.


Thanks in advance,

  Stefan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Resolving overloading loops for circular constraint graph

2009-09-09 Thread Martin Sulzmann 
Your example must loop because as you show below
the instance declaration leads to a cycle.

By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.

In any case, this is not a bug, you simply play with fire
once type functions show up in the instance context.
There are sufficient conditions to guarantee termination,
but they are fairly restrictive.

-Martin

2009/9/9 Stefan Holdermans ste...@cs.uu.nl

 Manuel, Simon,

 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 (also attached) 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?

 I'm not sure whether this is a known defect. If it isn't, I'd be more than
 happy to issue a report.

 Since this problem arises in a piece of very mission-critical code, I would
 be pleased to learn about any workarounds.

 Thanks in advance,

  Stefan
 ___
 Haskell-Cafe mailing list
 Haskell-Cafe@haskell.org
 http://www.haskell.org/mailman/listinfo/haskell-cafe

___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Re: [Haskell-cafe] Resolving overloading loops for circular constraint graph

2009-09-09 Thread Stefan Holdermans 

Dear Martin,


Your example must loop because as you show below
the instance declaration leads to a cycle.



By black-holing you probably mean co-induction. That is,
if the statement to proven appears again, we assume it must hold.
However, type classes are by default inductive, so there's no
easy fix to offer to your problem.


Yes, I meant coinductive resolving of overloading.

By that line of reasoning, the following should loop as well, but  
doesn't:


  {-# LANGUAGE FlexibleContexts #-}
  {-# LANGUAGE UndecidableInstances #-}

  class C a
  instance C ()
  instance (C (a, ()), C b) = C (a, b)

  f :: C (a, ()) = a - Int
  f _ = 2

  main ::   IO ()
  main = print (f   (3 :: Int))

Note: here I would accept looping behaviour as this program requires  
undecidable instances.



In any case, this is not a bug, you simply play with fire
once type functions show up in the instance context.
There are sufficient conditions to guarantee termination,
but they are fairly restrictive.


I disagree: it is a bug. I think the original program should require  
undecidable instances as well: indeed, the presence of the type family  
makes that the constraint is possibly no smaller than the instance  
head. However, without the undecidable-instance requirement (i.e., as  
it is now), I expect type checking to terminate.


Cheers,

  Stefan
___
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe