ndmitchell / record-dot-preprocessor

A preprocessor for a Haskell record syntax using dot
Other
129 stars 19 forks source link

Broken GADTs #12

Closed DoctorRyner closed 4 years ago

DoctorRyner commented 5 years ago

(0.2 version) It seems that it doesn't work with GADTs due to some parsing issue

data V3 a where
    V3 :: Num a => { x, y, z :: a } -> V3 a

It outputs that

parse error on input ‘Z.modifyField’
  |
6 |     V3 :: Num a=>{ x, y, z :: a } -> V3 a

While it works fine without a plugin

DoctorRyner commented 5 years ago

Also it compiles when use ExistentialQuantification ghc extension like that

data V3 a = Num a => V3 { x, y, z :: a }

but when you try to access using dot it says that

• No instance for (Z.HasField "x" (V3 Int) Int)
        arising from a use of ‘Z.getField’
    • In the expression: (Z.getField @"x" zero)
      In an equation for ‘test’: test = (Z.getField @"x" zero)
   |
11 | test = zero.x
ndmitchell commented 5 years ago

I think existential quantification and getField are incompatible - there's no way to write a function:

data V3 = forall a . Num a => V3 {x :: a}
getX :: V3 -> a

However, I'm not sure you are actually using existential quantification - it looks a lot more like data type contexts, see https://downloads.haskell.org/~ghc/7.8.3/docs/html/users_guide/data-type-extensions.html. What does the Num a => mean? Is having it on your type actually helpful?

So I suspect the answer is it can't work for existentials, you aren't actually using existentials. It could work for your code, but probably doesn't right now, and if it is a deprecated feature, its not a big priority to fix. I suspect it doesn't work for normal GADT syntax, and probably should do.

However, I'm not super sure on the Num a thing, so do let me know if you think I've confused myself.

DoctorRyner commented 5 years ago

The second example is just me experimenting. I want that my record could have a constraint for a polymorphic type, I used to use gadts for that (as in the first example) but it just doesn't work with this preprocessor

ndmitchell commented 5 years ago

The lack of GADTs is just a bug - worth fixing.

Why do you want to constrain the polymorphic type? Experience with that feature in Haskell has suggested it's almost never the right thing to do, and people have wanted to remove it from the language for a really long time. I don't think it has any fans, pretty much - it doesn't quite do what you might expect. Generally you would constrain the functions that operate on that type instead.

DoctorRyner commented 5 years ago

For example how it should work

data V3 a where
    V3 :: Num a => { x, y, z :: a } -> V3 a

zero :: Num a => V3 a
zero = V3 0 0 0

test1 :: V3 Float
test1 = zero -- Works

test2 :: V3 Int
test2 = V3 0 0 0 -- Works

test3 :: Int
test3 = x test2 -- Works

test4 :: Double
test4 = x zero -- Works

test5 :: V3 String -- Type error due to Num constraint
test5 = V3 "" "" ""

Why do you want to constrain the polymorphic type?

Why do we need constraints at all? Cuz something doesn't suppose to have inappropriate values especially if we can't use functions with it, it doesn't make sense and just confusing

ndmitchell commented 5 years ago

Ok, that does provide some benefit - a corner of Haskell I'd never seen. Should be possible to add support for. Thanks for educating me!

DoctorRyner commented 5 years ago

Thanks for educating me!

Don't joke like that :)

I just wanted some bug fix, thanks

ndmitchell commented 4 years ago

I think I've fixed this in HEAD. Let me know if it solves it for you, and if not let me know where it breaks now.

DoctorRyner commented 4 years ago

Thanks