CODEWITHSUNDEEP
haskell
A Sz
A Sz

Reputation: 1094

GHC cannot deduce (a1 ~ a) with GADTs and existential types

My code does not compile:

{-# LANGUAGE EmptyDataDecls, GADTs, RankNTypes  #-}

import Data.Ratio

data Ellipsoid
data Halfplane

data PointSet a where
    Halfplane :: RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Halfplane
    Ellipsoid :: RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Ellipsoid

type TestFunc =  RealFrac a => (a -> a -> a ->  Bool)

ellipsoid :: PointSet Ellipsoid -> TestFunc
ellipsoid (Ellipsoid a b c f r) = f' where f' z y x = ((x/a)^2 + (y/b)^2 + (z/c)^2) `f` r

halfplane :: PointSet Halfplane -> TestFunc
halfplane (Halfplane a b c f t) = f' where f' z y x = (a*x + b*y + c*z) `f` t

The error I get is:

Could not deduce (a1 ~ a)
[...]
Expected type: a -> a -> a -> Bool
  Actual type: a1 -> a1 -> a1 -> Bool
In the expression: f'
[...]

for both functions ellipsoid and halfplane.

I don't understand and am looking for an answer, why a cannot be equated with a1, both being RealFrac, or even better: why two different types (a ~ a1) are deduced?

Upvotes: 4

Views: 264

Answers (1)

cdk
cdk

Reputation: 6778

Your use of GADT with implicit forall is causing you grief. This is a good time to mention the "existential quantification with typeclass" anti-pattern

Since you've included the constraint RealFrac a in the definition of PointSet you're implicitly using forall like this:

data PointSet a where
    Halfplane :: forall a. RealFrac a => a -> a -> a -> (a -> a -> Bool) -> a -> PointSet HalfPlane
    Ellipsoid :: forall a. RealFrac a => ...

The same applies to TestFunc:

type TestFunc = forall a. RealFrac a => a -> a -> a -> Bool

This is why GHC coerced you into adding the RankNTypes extension.

Because of forall the a in the constructors for PointSet cannot possibly unify with the a in TestFunc since the a in PointSet is some specific instance of RealFrac, but TestFunc is a function that is required to work for any a.

This difference between the specific type a and the universally quantified forall a. a causes GHC to deduce two different types a and a1.

The solution? Scrap all this existential nonsense. Apply the typeclass constraints where and when they're needed:

{-# LANGUAGE DataKinds, GADTs, KindSignatures #-}

data Shape = Halfplane | Ellipsoid -- promoted via DataKinds

data PointSet (s :: Shape) a where
    Halfplane :: a -> a -> a -> (a -> a -> Bool) -> a -> PointSet Halfplane a
    Ellipsoid :: ...

type TestFunc a = a -> a -> a -> Bool

ellipsoid :: RealFrac a => PointSet Ellipsoid a -> TestFunc a
ellipsoid (Ellipsoid a b c f r) = f' where f' = ...

Now PointSet takes 2 parameters: a phantom type s :: Shape which has kind Shape (kinds are the types of types) and a which is the same as your original example, except as an explicit argument to PointSet it is no longer implicitly existentially quantified.

To address your last point, the a and a1 in the error message are not "both being RealFrac. RealFrac is not a type, it is a typeclass. a and a1 are two potentially distinct types that both happen to be instances of RealFrac.

That said, unless you are making use of the more expressive type of PointSet there is a much simpler solution.

data PointSet a
    = Halfplane a a a (a -> a -> Bool) a
    | Ellipsoid a a a (a -> a -> Bool) a

testFunc :: RealFrac a => PointSet a -> TestFunc a
testFunc (Ellipsoid a b c f r) = f' where f' = ...
testFunc (Halfplane a b c f t) = f' where f' = ...

Upvotes: 6

Related Questions