TypeFamillies and UndecidableInstances - why?
When I tried to do something like:
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-}
class Test a where type TestMonad a :: * -> * from :: a b -> TestMonad a b to :: TestMonad a b -> a b
data Testable a b = Testable (a b)
instance (Test a, Functor (TestMonad a)) => Functor (Testable a) where f `fmap` Testable v = Testable $! (to . fmap f . from) v
It asks for adding UndecidableInstances as: test.hs:11:0: Constraint is no smaller than the instance head in the constraint: Functor (TestMonad a) (Use -XUndecidableInstances to permit this) In the instance declaration for `Functor (Testable a)' What is undecidable? a is bound so TestMonad a should be bound so Functor (TestMonad a) should be valid. Is it a bug/missing feature in ghc or do I fail to see something? Regards
On Jun 22, 2010, at 21:41 , Maciej Piechotka wrote:
test.hs:11:0: Constraint is no smaller than the instance head in the constraint: Functor (TestMonad a) (Use -XUndecidableInstances to permit this) In the instance declaration for `Functor (Testable a)'
What is undecidable? a is bound so TestMonad a should be bound so Functor (TestMonad a) should be valid.
I *think* the point of the error message is that Functor (TestMonad a) is a tautology, so including it doesn't actually constrain the instance (which in GHC-ese is "Constraint is no smaller than the instance head"). In short, GHC thinks you're being tricky in a way it can't understand, because otherwise there's no point in including the constraint, so it's telling you that being tricky requires UndecidableInstances. -- brandon s. allbery [solaris,freebsd,perl,pugs,haskell] allbery@kf8nh.com system administrator [openafs,heimdal,too many hats] allbery@ece.cmu.edu electrical and computer engineering, carnegie mellon university KF8NH
On Tue, 2010-06-22 at 21:51 -0400, Brandon S. Allbery KF8NH wrote:
On Jun 22, 2010, at 21:41 , Maciej Piechotka wrote:
test.hs:11:0: Constraint is no smaller than the instance head in the constraint: Functor (TestMonad a) (Use -XUndecidableInstances to permit this) In the instance declaration for `Functor (Testable a)'
What is undecidable? a is bound so TestMonad a should be bound so Functor (TestMonad a) should be valid.
I *think* the point of the error message is that Functor (TestMonad a) is a tautology, so including it doesn't actually constrain the instance (which in GHC-ese is "Constraint is no smaller than the instance head"). In short, GHC thinks you're being tricky in a way it can't understand, because otherwise there's no point in including the constraint, so it's telling you that being tricky requires UndecidableInstances.
I'm sorry but how "Functor (TestMonad a) is a tautology"? It cannot be derived from other constraints (in and outside this class). Unless you mean that GHC thinks it is tautology. Regards
On Wednesday 23 June 2010 03:41:47, Maciej Piechotka wrote:
When I tried to do something like:
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-}
class Test a where type TestMonad a :: * -> * from :: a b -> TestMonad a b to :: TestMonad a b -> a b
data Testable a b = Testable (a b)
instance (Test a, Functor (TestMonad a)) => Functor (Testable a) where f `fmap` Testable v = Testable $! (to . fmap f . from) v
It asks for adding UndecidableInstances as:
test.hs:11:0: Constraint is no smaller than the instance head in the constraint: Functor (TestMonad a) (Use -XUndecidableInstances to permit this) In the instance declaration for `Functor (Testable a)'
What is undecidable? a is bound so TestMonad a should be bound so Functor (TestMonad a) should be valid.
Is it a bug/missing feature in ghc or do I fail to see something?
Regards
The constraint contains one type variable, as does the instance head, so the compiler can't be sure that type checking will terminate. Here, UndeciableInstances means, "type checking will terminate, go ahead".
On Wed, 23 Jun 2010, Maciej Piechotka wrote:
When I tried to do something like:
{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE TypeFamilies #-}
class Test a where type TestMonad a :: * -> * from :: a b -> TestMonad a b to :: TestMonad a b -> a b
data Testable a b = Testable (a b)
instance (Test a, Functor (TestMonad a)) => Functor (Testable a) where f `fmap` Testable v = Testable $! (to . fmap f . from) v
It asks for adding UndecidableInstances as:
test.hs:11:0: Constraint is no smaller than the instance head in the constraint: Functor (TestMonad a) (Use -XUndecidableInstances to permit this) In the instance declaration for `Functor (Testable a)'
Basically, the compiler starts with "Is `Testable a` a Functor?" and ends with "Is `a` a Test and (figure out what `TestMonad a`) a Functor?" The second question is more work to do than it started with. The `Test a` constraint is fine, because you're at least narrowing down the type in question. But `TestMonad a` is a type function that could be literally anything, including `Testable a` itself, which would leave us at: instance (Functor (Testable a)) => Functor (Testable a) Which is obviously problematic. Friendly, --Christopher Lane Hinson
participants (4)
-
Brandon S. Allbery KF8NH -
Christopher Lane Hinson -
Daniel Fischer -
Maciej Piechotka