Derrivations and implications

Learn
#1

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?

#2

The following compiles:

{-# 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
1 Like
#3

Hmm… :thinking: 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…

#4

I used GHC 8.10.4 too. A single Haskell file, compiled directly with ghc X.hs, no Cabal, no nothing.

#5

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.

1 Like
#6

That’s where I fell into trap. Now I see it.