toP without Maybe

1
2
3
4
toP :: SingI a => Vector a1 -> Point a a1
toP = withSing go where
  go :: Sing d -> Vector a -> Point d a
  go _ v = Point v
4:3: Error: Eta reduce
Found:
go _ v = Point v
Why not:
go _ = Point