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

Question

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 am getting 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 ellipsoidand halfplane.

I don’t understand and am looking for an answer why ait cannot be equated to a1, both are RealFracor even better: why are two different types ( a ~ a1) derived ?

Answer 1

Your use GADTwith implicit forallcauses you grief. This is a good time to mention the "existential quantification using typeclass" anti-pattern

Since you included the restriction RealFrac ain the definition PointSet, you are implicitly using the forallfollowing:

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

TestFunc:

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

GHC RankNTypes.

- forall a PointSet a TestFunc, a in PointSet RealFrac, TestFunc - , a.

a forall a. a GHC a a1.

? . , , :

{-# 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' = ...

PointSet 2 : phantom s :: Shape, Shape ( - ) a, , PointSet, .

, a a1 " RealFrac. RealFrac , . a a1 , RealFrac.

, PointSet, .

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' = ...