Here's another fun question. The following module is legal in GC, and does what you would expect. \begin{code} {-# LANGUAGE FlexibleInstances, OverlappingInstances #-} module Parametric where class IsInt a where isInt :: a -> Bool instance IsInt a where isInt _ = False instance IsInt Int where isInt _ = True myList1 :: IsInt a => a -> [a] myList1 x = if isInt x then [x] else [x, x] \end{code} Would the following module be legal under the proposal? If so, parametricity is gone, because you can define typecase without any constraints. \begin{code} {-# LANGUAGE ScopedTypeVariables, FlexibleInstances, OverlappingInstances, LocalInstances #-} module NotParametric where import Parametric myList2 :: a -> [a] myList2 (x :: a) = let instance IsInt a where isInt _ = False in let instance IsInt Int where isInt _ = True in myList1 x -- the IsInt constraint should be discharged by the local instances \end{code} The only way I see of avoiding this is if local instances can't discharge a constraint; that is, a local instance can only shadow an existing instance. It can't create an instance for a type that didn't already have one. Or maybe there's just a bad interaction with flexible/overlapping instances, but the extension seems less useful without these. -- Jason McCarty <jmccarty@sent.com>