relaxed instance termination test
authorRoss Paterson <ross@soi.city.ac.uk>
Mon, 6 Feb 2006 11:16:51 +0000 (11:16 +0000)
committerRoss Paterson <ross@soi.city.ac.uk>
Mon, 6 Feb 2006 11:16:51 +0000 (11:16 +0000)
commit1cdafe99abae1628f34ca8c064e3a8c0fcdbd079
treec269a6e4043214113c94a620096b93de886a8641
parent89a16d32889b369508faa8a069abffa3257d3a4f
relaxed instance termination test

With -fglasgow-exts but not -fallow-undecidable-instances, GHC 6.4
requires that instances be of the following form:

 (1) each assertion in the context must constrain distinct variables
     mentioned in the head, and

 (2) at least one argument of the head must be a non-variable type.

This patch replaces these rules with the requirement that each assertion
in the context satisfy

 (1) no variable has more occurrences in the assertion than in the head, and

 (2) the assertion has fewer constructors and variables (taken together
     and counting repetitions) than the head.

This allows all instances permitted by the old rule, plus such instances as

       instance C a
       instance Show (s a) => Show (Sized s a)
       instance (Eq a, Show b) => C2 a b
       instance C2 Int a => C3 Bool [a]
       instance C2 Int a => C3 [a] b
       instance C4 a a => C4 [a] [a]

but still ensures that under any substitution assertions in the context
will be smaller than the head, so context reduction must terminate.

This is probably the best we can do if we consider each instance in
isolation.
ghc/compiler/typecheck/TcInstDcls.lhs
ghc/compiler/typecheck/TcMType.lhs