I am learning haskell and come up with code that resembles the following:
class A a b where
ident :: a -> b
class B a
-- every type is B
instance (forall a . a) => B a
-- Any a that is B is sufficient to define A
-- This means that B implies A (correct?)
instance (forall a . B a) => A a a where
ident a = a
-- So anything that requires a value to be B
-- implicitly says that any B is A & and there exist
-- 'common' implementation that compiler can pick up
-- Which means that I can use Bs as As
oops :: B a => a -> a
oops a = ident a
_ = oops ""
But ghc doesnât follow this reasoning and shows two errors:
Could not deduce: a2 arising from a use of âidentâ from the context: B a
Could not deduce: a arising from a use of âoopsâ. In the expression: oops ""
Am I paying not enough attention and there is a reason why this code is incorrect, or is it ghc?
{-# language RankNTypes
, MultiParamTypeClasses
, FlexibleInstances
, QuantifiedConstraints
#-}
module X where
class A a b where
ident :: a -> b
class B a
instance (forall a . a) => B a
instance forall a . B a => A a a where
ident a = a
oops :: B a => a -> a
oops a = ident a
Hmm⌠Maybe the crucial mismatch here is the difference in compiler versions. I am on ghc 8.10.4, just tried your code (with all extensions enabled, naturally) and it lead to the same error I had. What is your version?
I also have DataKinds and PolyKinds (and bunch of other extensions) enabled which are used elsewhere in my code, so I wonder whether it can cause interferenceâŚ
For me @kindaroâs code compiles too with GHC 8.10.4, but running oops on an input gives the described error. I find some parts of your code very strange. I would expect something like:
class A a b where
ident :: a -> b
class B a
-- every type is B
instance B a -- forall is implicit
-- Any a that is B is sufficient to define A
-- This means that B implies A (correct?)
instance B a => A a a where -- again forall is implicit
ident a = a
-- So anything that requires a value to be B
-- implicitly says that any B is A & and there exist
-- 'common' implementation that compiler can pick up
-- Which means that I can use Bs as As
oops :: B a => a -> a
oops a = ident a
This code compiles and runs without errors.
The QuantifiedConstraints extensions allows your code to compile but I donât think it does what you think it does.
The line instance (forall a . a) => B a is (alpha) equivalent to instance (forall b. b) => B a, I think it means: âIf for all constraints b the constraint b holds, then for all types a the constraint B a holds.â Note that the first a variable is not a type variable but a constraint variable and it is not the same as the variable that is applied to B.
The other line instance forall a. B a => A a a is correct, because it is equivalent to instance forall a. (B a => A a a) which is equivalent to instance B a => A a a.
Finally, you should probably never write instances which hold for all types like instance B a because they only complicate things and I think they have no actual value.