Selda: confused about type signtures

newer
In which format should GHC expose...

older
Munich Haskell Meeting, 2018-04-26...

Marc Busqué

20 Apr 2018 20 Apr '18

2:33 p.m.

Hi! I'm using [selda](https://hackage.haskell.org/package/selda) package in order to deal with database backends. Selda uses `TypeOperators` language extension, and it introduces `:*:` type operator constructor which take concrete types like `RowID` or `Text` . It also has a `Table` type constructor which takes anything built with `:*:`). On the other hand, `SeldaM` is selda custom monad transformer with `IO` at the bottom. I have following helper function which just wraps a call to the SQLite backend. `dBPath` is just the database file path: ``` withDB :: SeldaM a -> IO a withDB act = do path <- dBPath withSQLite path act ``` I want to wrap selda API in custom functions to be more resilient to changes. Right now I'm trying to abstract selecting all rows for a given table (maybe it seems brittle, but it is just a toy project in order to learn Haskell): ``` list table = withDB $ query (select table) ``` Not adding a type signature to `list` produces following compilation error: ``` • Non type-variable argument in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a) (Use FlexibleContexts to permit this) • When checking the inferred type list :: forall s a. (selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a), selda-0.1.12.1:Database.Selda.Compile.Result (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)] ``` If I try to add what I think would be the correct signature: ``` list :: Table a -> IO [a] ``` The error changes to: ``` • Couldn't match type ‘a’ with ‘selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’ ‘a’ is a rigid type variable bound by the type signature for: list :: forall a. Table a -> IO [a] at src/Hedger/Category.hs:35:1-25 Expected type: SeldaM [a] Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)] • In the second argument of ‘($)’, namely ‘query (select table)’ In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Category.hs:36:6) list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1) | 36 | list table = withDB $ query (select table) ``` However, if I constraint the type signature to act just for a given table, it compiles without errors: ``` type CategoriesSchema = RowID:*:Text list :: Table CategoriesSchema -> IO [CategoriesSchema] ``` Why is that it works with concrete types but not with a type variable that takes the same concrete type in its both placeholders? Thanks in advance, Marc Busqué http://waiting-for-dev.github.io/about/

Show replies by date

Tom Ellis

20 Apr 20 Apr

2:39 p.m.

On Fri, Apr 20, 2018 at 08:33:10PM +0200, Marc Busqué wrote:

...

Not adding a type signature to `list` produces following compilation error:

[...]

...

(Use FlexibleContexts to permit this)

Why is that it works with concrete types but not with a type variable that takes the same concrete type in its both placeholders?

Did you try applying the suggested fix? Explicitly, add {-# LANGUAGE FlexibleContexts #-} at the top of your file to permit this.

Marc Busqué

2:46 p.m.

On Fri, 20 Apr 2018, Tom Ellis wrote:

...

Did you try applying the suggested fix? Explicitly, add

{-# LANGUAGE FlexibleContexts #-}

at the top of your file to permit this.

It doesn't work neither. In this case the error is: ``` • Couldn't match type ‘selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’ with ‘selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)’ Expected type: Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)] Actual type: Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)] NB: ‘selda-0.1.12.1:Database.Selda.Compile.Res’ is a type function, and may not be injective The type variable ‘s0’ is ambiguous • In the ambiguity check for the inferred type for ‘list’ To defer the ambiguity check to use sites, enable AllowAmbiguousTypes When checking the inferred type list :: forall s a. (selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a), selda-0.1.12.1:Database.Selda.Compile.Result (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)] | 36 | list table = withDB $ query (select table) ``` Anyway, I'm more interested in understanding an explicit type signature, in this case. Marc Busqué http://waiting-for-dev.github.io/about/

Brandon Allbery

2:47 p.m.

The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here, but your type signature just says a, you will get a type error exactly as you did. "a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work there. On Fri, Apr 20, 2018 at 2:33 PM, Marc Busqué wrote:

...

Hi!

I'm using [selda](https://hackage.haskell.org/package/selda) package in order to deal with database backends.

Selda uses `TypeOperators` language extension, and it introduces `:*:` type operator constructor which take concrete types like `RowID` or `Text` . It also has a `Table` type constructor which takes anything built with `:*:`). On the other hand, `SeldaM` is selda custom monad transformer with `IO` at the bottom.

I have following helper function which just wraps a call to the SQLite backend. `dBPath` is just the database file path:

``` withDB :: SeldaM a -> IO a withDB act = do path <- dBPath withSQLite path act ```

I want to wrap selda API in custom functions to be more resilient to changes. Right now I'm trying to abstract selecting all rows for a given table (maybe it seems brittle, but it is just a toy project in order to learn Haskell):

``` list table = withDB $ query (select table) ```

Not adding a type signature to `list` produces following compilation error:

``` • Non type-variable argument in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a) (Use FlexibleContexts to permit this) • When checking the inferred type list :: forall s a. (selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a), selda-0.1.12.1:Database.Selda.Compile.Result (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)] ```

If I try to add what I think would be the correct signature:

``` list :: Table a -> IO [a] ```

The error changes to:

``` • Couldn't match type ‘a’ with ‘selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’ ‘a’ is a rigid type variable bound by the type signature for: list :: forall a. Table a -> IO [a] at src/Hedger/Category.hs:35:1-25 Expected type: SeldaM [a] Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)] • In the second argument of ‘($)’, namely ‘query (select table)’ In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Category.hs:36:6) list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1) | 36 | list table = withDB $ query (select table) ```

However, if I constraint the type signature to act just for a given table, it compiles without errors:

``` type CategoriesSchema = RowID:*:Text list :: Table CategoriesSchema -> IO [CategoriesSchema] ```

Why is that it works with concrete types but not with a type variable that takes the same concrete type in its both placeholders?

Thanks in advance,

Marc Busqué http://waiting-for-dev.github.io/about/ _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Marc Busqué

3:20 p.m.

On Fri, 20 Apr 2018, Brandon Allbery wrote:

...

The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here, but your type signature just says a, you will get a type error exactly as you did. "a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work there.

Thanks! That was an illuminating answer :) Marc Busqué http://waiting-for-dev.github.io/about/

Marc Busqué

22 Apr 22 Apr

2:21 p.m.

On Fri, 20 Apr 2018, Brandon Allbery wrote:

...

The more precise answer to your question is that an explicit type signature is taken as exact. If the type needed is some (Ctx a => a), as here, but your type signature just says a, you will get a type error exactly as you did. "a" there does not mean "figure out a type for me". It means *any type at all*. Including Void, (), Int, etc., which one would not expect to work there.

I'm still in troubles with this... If I add `FlexibleContexts` and `AllowAmbiguosTypes` extensions, I can compile the program and ask for the type of `list`: ``` :t list --- list --- :: (selda-0.1.12.1:Database.Selda.Compile.Result --- (selda-0.1.12.1:Database.Selda.Column.Cols s a), --- selda-0.1.12.1:Database.Selda.Column.Columns --- (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => --- selda-0.1.12.1:Database.Selda.Table.Table a --- -> IO --- [selda-0.1.12.1:Database.Selda.Compile.Res --- (selda-0.1.12.1:Database.Selda.Column.Cols s a)] ``` However, manually adding this same type: ``` list :: (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table) ``` results in a compilation error: ``` • Couldn't match type ‘Res (Cols s0 a)’ with ‘Res (Cols s a)’ Expected type: IO [Res (Cols s a)] Actual type: IO [Res (Cols s0 a)] NB: ‘Res’ is a type function, and may not be injective The type variable ‘s0’ is ambiguous • In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Category.hs:44:6) list :: Table a -> IO [Res (Cols s a)] (bound at src/Hedger/Category.hs:44:1) | 44 | list table = withDB $ query (select table) ``` I'm pretty sure that my error is related with what is exposed in this page in the wiki: https://wiki.haskell.org/GHC/TypeSigsAndAmbiguity But I'm not sure about how I could fix that. At the end of the article it is said that this only happen in programs that "they could never really work". But, if I'm not missing something, that function does work. I have tried it with the auto-inferred signature way and it indeed can list rows for different database tables. I leave here more info just in case it is useful: ``` :t select --- select :: Columns (Cols s a) => Table a -> Query s (Cols s a) :t query --- query :: (Result a, MonadSelda m) => Query s a -> m [Res a] :t withDB --- withDB :: SeldaM a -> IO a :info Columns class Columns a where --- selda-0.1.12.1:Database.Selda.Column.toTup :: [ColName] -> a --- selda-0.1.12.1:Database.Selda.Column.fromTup :: a --- -> [selda-0.1.12.1:Database.Selda.Exp.SomeCol --- selda-0.1.12.1:Database.Selda.SQL.SQL] --- {-# MINIMAL toTup, fromTup #-} --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’ --- instance forall k (s :: k) a. Columns (Col s a) --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’ --- instance forall k b (s :: k) a. --- Columns b => --- Columns (Col s a :*: b) --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’ :info Cols --- type family Cols (s :: k) a :: * --- where --- [k, (s :: k), a, b] Cols k s (a :*: b) = Col s a :*: Cols s b --- [k, (s :: k), a] Cols k s a = Col s a --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Column’ :info Result --- class base-4.10.1.0:Data.Typeable.Internal.Typeable (Res r) => --- Result r where --- type family Res r :: * --- selda-0.1.12.1:Database.Selda.Compile.toRes :: Data.Proxy.Proxy r --- -> [selda-0.1.12.1:Database.Selda.SqlType.SqlValue] --- -> Res r --- selda-0.1.12.1:Database.Selda.Compile.finalCols :: r --- -> [selda-0.1.12.1:Database.Selda.Exp.SomeCol --- selda-0.1.12.1:Database.Selda.SQL.SQL] --- {-# MINIMAL toRes, finalCols #-} --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ --- instance SqlType a => Result (Col s a) --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ --- instance (SqlType a, Result b) => Result (Col s a :*: b) --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ :info Res --- class base-4.10.1.0:Data.Typeable.Internal.Typeable (Res r) => --- Result r where --- type family Res r :: * --- ... --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ --- type instance Res (Col s a) = a --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ --- type instance Res (Col s a :*: b) = a :*: Res b --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Compile’ :info Table --- type role Table phantom --- data Table a --- = selda-0.1.12.1:Database.Selda.Table.Table {selda-0.1.12.1:Database.Selda.Table.tableName :: TableName, --- selda-0.1.12.1:Database.Selda.Table.tableCols :: [selda-0.1.12.1:Database.Selda.Table.ColInfo], --- selda-0.1.12.1:Database.Selda.Table.tableHasAutoPK :: Bool} --- -- Defined in ‘selda-0.1.12.1:Database.Selda.Table’ ``` Marc Busqué http://waiting-for-dev.github.io/about/

...

On Fri, Apr 20, 2018 at 2:33 PM, Marc Busqué wrote: Hi!

I'm using [selda](https://hackage.haskell.org/package/selda) package in order to deal with database backends.

Selda uses `TypeOperators` language extension, and it introduces `:*:` type operator constructor which take concrete types like `RowID` or `Text` . It also has a `Table` type constructor which takes anything built with `:*:`). On the other hand, `SeldaM` is selda custom monad transformer with `IO` at the bottom.

I have following helper function which just wraps a call to the SQLite backend. `dBPath` is just the database file path:

``` withDB :: SeldaM a -> IO a withDB act = do path <- dBPath withSQLite path act ```

I want to wrap selda API in custom functions to be more resilient to changes. Right now I'm trying to abstract selecting all rows for a given table (maybe it seems brittle, but it is just a toy project in order to learn Haskell):

``` list table = withDB $ query (select table) ```

Not adding a type signature to `list` produces following compilation error:

``` • Non type-variable argument in the constraint: selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a) (Use FlexibleContexts to permit this) • When checking the inferred type list :: forall s a. (selda-0.1.12.1:Database.Selda.Column.Columns (selda-0.1.12.1:Database.Selda.Column.Cols s a), selda-0.1.12.1:Database.Selda.Compile.Result (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => Table a -> IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s a)] ```

If I try to add what I think would be the correct signature:

``` list :: Table a -> IO [a] ```

The error changes to:

``` • Couldn't match type ‘a’ with ‘selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)’ ‘a’ is a rigid type variable bound by the type signature for: list :: forall a. Table a -> IO [a] at src/Hedger/Category.hs:35:1-25 Expected type: SeldaM [a] Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT IO [selda-0.1.12.1:Database.Selda.Compile.Res (selda-0.1.12.1:Database.Selda.Column.Cols s0 a)] • In the second argument of ‘($)’, namely ‘query (select table)’ In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Category.hs:36:6) list :: Table a -> IO [a] (bound at src/Hedger/Category.hs:36:1) | 36 | list table = withDB $ query (select table) ```

However, if I constraint the type signature to act just for a given table, it compiles without errors:

``` type CategoriesSchema = RowID:*:Text list :: Table CategoriesSchema -> IO [CategoriesSchema] ```

Why is that it works with concrete types but not with a type variable that takes the same concrete type in its both placeholders?

Thanks in advance,

Marc Busqué http://waiting-for-dev.github.io/about/ _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

-- brandon s allbery kf8nh sine nomine associates allbery.b@gmail.com ballbery@sinenomine.net unix, openafs, kerberos, infrastructure, xmonad http://sinenomine.net

Tom Ellis

3:18 p.m.

On Sun, Apr 22, 2018 at 08:21:11PM +0200, Marc Busqué wrote:

...

If I add `FlexibleContexts` and `AllowAmbiguosTypes` extensions, I can compile the program and ask for the type of `list`:

``` :t list --- list --- :: (selda-0.1.12.1:Database.Selda.Compile.Result --- (selda-0.1.12.1:Database.Selda.Column.Cols s a), --- selda-0.1.12.1:Database.Selda.Column.Columns --- (selda-0.1.12.1:Database.Selda.Column.Cols s a)) => --- selda-0.1.12.1:Database.Selda.Table.Table a --- -> IO --- [selda-0.1.12.1:Database.Selda.Compile.Res --- (selda-0.1.12.1:Database.Selda.Column.Cols s a)] ```

However, manually adding this same type:

``` list :: (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table) ```

results in a compilation error:

Unless I am much mistaken `Cols s a` is just `a`[1,2]. That explains why the type is ambiguous. There's nothing that fixes `s`.

...

But I'm not sure about how I could fix that. At the end of the article it is said that this only happen in programs that "they could never really work". But, if I'm not missing something, that function does work. I have tried it with the auto-inferred signature way and it indeed can list rows for different database tables.

Can you show us a minimal example of `list` working? I'm quite confused about how it could work. Tom [1] https://www.stackage.org/haddock/lts-9.14/selda-0.1.11.1/src/Database.Selda....) [2] https://www.stackage.org/haddock/lts-9.14/selda-0.1.11.1/Database-Selda.html...

Marc Busqué

23 Apr 23 Apr

3:23 a.m.

On Sun, 22 Apr 2018, Tom Ellis wrote:

...

Unless I am much mistaken `Cols s a` is just `a`[1,2]. That explains why the type is ambiguous. There's nothing that fixes `s`.

I also thought that, but if I substitute `Cols s a` by `a`, then the compilation error is: ``` • Couldn't match type ‘Res (Cols s0 a)’ with ‘Res a’ Expected type: IO [Res a] Actual type: IO [Res (Cols s0 a)] NB: ‘Res’ is a type function, and may not be injective The type variable ‘s0’ is ambiguous • In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Category.hs:44:6) list :: Table a -> IO [Res a] (bound at src/Hedger/Category.hs:44:1) | 44 | list table = withDB $ query (select table) ``` Also, notice that the inferred type does differentiate between `Cols s a` and `a`.

...

Can you show us a minimal example of `list` working? I'm quite confused about how it could work.

``` type CategoriesSchema = RowID:*:Text type ExpensesSchema = RowID:*:Text:*:Double:*:RowID categories:: Table (CategoriesSchema) (categories, categoryID :*: rest) = tableWithSelectors "categories" $ autoPrimary "id" :*: required "name" expenses:: Table (ExpensesSchema) expenses = table "expenses" $ autoPrimary "id" :*: required "name" :*: required "amount" :*: required "category_id" `fk` (categories, categoryID) withDB (tryCreateTable categories) withDB (tryCreateTable expenses) withDB $ insert_ categories [ def :*: "foo" ] list categories --- [1 :*: "foo"] list expenses --- [] Marc Busqué http://waiting-for-dev.github.io/about/

Tom Ellis

8:16 a.m.

On Mon, Apr 23, 2018 at 09:23:58AM +0200, Marc Busqué wrote:

...

On Sun, 22 Apr 2018, Tom Ellis wrote:

...
Unless I am much mistaken `Cols s a` is just `a`[1,2]. That explains why the type is ambiguous. There's nothing that fixes `s`.

I also thought that, but if I substitute `Cols s a` by `a`, then the compilation error is:

I had an error in what I said and also it was imprecise. It's `Res (Cols s a)` which is `a`, but only in the cases where you're actually going to use it, and the compiler cannot take that into account when solving the constraint. Anyway, as Li-yao Xia points out in a sibling message, the type variable `s` in not constrained and therefore it seems impossible to solve.

...

Also, notice that the inferred type does differentiate between `Cols s a` and `a`.

...
Can you show us a minimal example of `list` working? I'm quite confused about how it could work. [...]

Thanks, but could you send a full working version that includes a definition of `list`? I can't replicate what you've done on my end. Tom

Tom Ellis

8:25 a.m.

On Mon, Apr 23, 2018 at 01:16:50PM +0100, Tom Ellis wrote:

...

Thanks, but could you send a full working version that includes a definition of `list`? I can't replicate what you've done on my end.

And what GHC version are you using? I can't replicate this on 7.10 or 8.0.

Marc Busqué

10:55 a.m.

On Mon, 23 Apr 2018, Tom Ellis wrote:

...

And what GHC version are you using? I can't replicate this on 7.10 or 8.0.

I'm on 8.2.2. Marc Busqué http://waiting-for-dev.github.io/about/

Marc Busqué

10:54 a.m.

On Mon, 23 Apr 2018, Tom Ellis wrote:

...

I had an error in what I said and also it was imprecise. It's `Res (Cols s a)` which is `a`, but only in the cases where you're actually going to use it, and the compiler cannot take that into account when solving the constraint. Anyway, as Li-yao Xia points out in a sibling message, the type variable `s` in not constrained and therefore it seems impossible to solve.

Thanks Tom for your reply. In this case the error is: ``` • Couldn't match type ‘a’ with ‘Res (Cols s0 a)’ ‘a’ is a rigid type variable bound by the type signature for: list :: forall s a. (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [a] at src/Hedger/Backend.hs:24:1-69 Expected type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaM [a] Actual type: selda-0.1.12.1:Database.Selda.Backend.Internal.SeldaT IO [Res (Cols s0 a)] • In the second argument of ‘($)’, namely ‘query (select table)’ In the expression: withDB $ query (select table) In an equation for ‘list’: list table = withDB $ query (select table) • Relevant bindings include table :: Table a (bound at src/Hedger/Backend.hs:25:6) list :: Table a -> IO [a] (bound at src/Hedger/Backend.hs:25:1) | 25 | list table = withDB $ query (select table) ```

...

Thanks, but could you send a full working version that includes a definition of `list`? I can't replicate what you've done on my end.

I have pushed the repo to Github: https://github.com/waiting-for-dev/hedger Important code is in `src/Hedger/` directory. `Backend.hs` is where `list` is defined. Right now it has its type signature commented out so that it compiles thanks to `AllowAmbiguosTypes` and `FlexibleContexts`. `Category.hs` has the function `listCategories` which uses `list`. Anyway, from `ghci` one can just call `list categories` or `list expenses`. There is also a helper function `addCategory` to add a category record just providing its name (from `ghci`, `OverloadedStrings` must be loaded). In `Migration.hs` is where `categories` and `expenses` tables are created. Marc Busqué http://waiting-for-dev.github.io/about/

Tom Ellis

12:48 p.m.

On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:

...

On Mon, 23 Apr 2018, Tom Ellis wrote:

...
I had an error in what I said and also it was imprecise. It's `Res (Cols s a)` which is `a`, but only in the cases where you're actually going to use it, and the compiler cannot take that into account when solving the constraint. Anyway, as Li-yao Xia points out in a sibling message, the type variable `s` in not constrained and therefore it seems impossible to solve.

I have pushed the repo to Github:

https://github.com/waiting-for-dev/hedger

Thanks for that Marc, it's very helpful. I extracted the parts that are relevant to the problem and created a version that doesn't depend on Selda: https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3 I think I now understand what the situation is. Interestingly your code works on 8.0 but not 7.10. Contrary to my earlier presumptions, the compiler *is* able to give a type to `list` because `Cols` is a closed type family. I suppose it can determine that `Cols s a` does not actually depend on `s` so giving list the type (Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a) is fine. The type of `s` will never be needed. When `list` is applied to `categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of what `s` is. Subtly changing the definition of Cols will break things. For example, if you add the clause Cols () a = Col Int a then you won't be able to define `list` any more, even though `Res (Cols s a)` is still just `a` because the `Columns (Cols s a)` instance might then depend on what `s` is. On the other hand, I do not yet understand why you cannot provide an explicit signature for `list`. I suspect this is some hairy compiler bug. Either it should be possible to give `list` its inferred type or it should be forbidden. It's probably worth filing an issue about this on GHC Trac. I would be interested to hear Li-yao's thoughts on the matter. Incidentally, this is why I try to avoid type families as much as possible. When they go wrong it's very hard to understand why, and indeed when they go right it's also very hard to understand why. Tom

Marc Busqué

2:08 p.m.

Tom, thank you very much for your deep inspection. Your gist can be really helpful in trying to understand the problem. I will study it carefully. I have been reading books about Haskell and also Category Theory for some months, but I have just started coding few weeks ago, so I'm bit overwhelmed about having found a compiler bug so soon :D I'll look into all of this and also about Li-yao recommendations and if it is suitable I'll fill the issue and also report here. Marc Busqué http://waiting-for-dev.github.io/about/ On Mon, 23 Apr 2018, Tom Ellis wrote:

...

On Mon, Apr 23, 2018 at 04:54:36PM +0200, Marc Busqué wrote:

...
On Mon, 23 Apr 2018, Tom Ellis wrote:

...
I had an error in what I said and also it was imprecise. It's `Res (Cols s a)` which is `a`, but only in the cases where you're actually going to use it, and the compiler cannot take that into account when solving the constraint. Anyway, as Li-yao Xia points out in a sibling message, the type variable `s` in not constrained and therefore it seems impossible to solve.

I have pushed the repo to Github:

https://github.com/waiting-for-dev/hedger

Thanks for that Marc, it's very helpful. I extracted the parts that are relevant to the problem and created a version that doesn't depend on Selda:

https://gist.github.com/tomjaguarpaw/f4db46671e2f39b790a25b8907dc53a3

I think I now understand what the situation is. Interestingly your code works on 8.0 but not 7.10.

Contrary to my earlier presumptions, the compiler *is* able to give a type to `list` because `Cols` is a closed type family. I suppose it can determine that `Cols s a` does not actually depend on `s` so giving list the type

(Result (Cols s a), Columns (Cols s a)) => Table a -> Res (Cols s a)

is fine. The type of `s` will never be needed. When `list` is applied to `categories` then `a` is fixed and `Res (Cols s a)` is fixed, regardless of what `s` is.

Subtly changing the definition of Cols will break things. For example, if you add the clause

Cols () a = Col Int a

then you won't be able to define `list` any more, even though `Res (Cols s a)` is still just `a` because the `Columns (Cols s a)` instance might then depend on what `s` is.

On the other hand, I do not yet understand why you cannot provide an explicit signature for `list`. I suspect this is some hairy compiler bug. Either it should be possible to give `list` its inferred type or it should be forbidden. It's probably worth filing an issue about this on GHC Trac. I would be interested to hear Li-yao's thoughts on the matter.

Incidentally, this is why I try to avoid type families as much as possible. When they go wrong it's very hard to understand why, and indeed when they go right it's also very hard to understand why.

Tom _______________________________________________ Haskell-Cafe mailing list To (un)subscribe, modify options or view archives go to: http://mail.haskell.org/cgi-bin/mailman/listinfo/haskell-cafe Only members subscribed via the mailman list are allowed to post.

Tom Ellis

2:16 p.m.

Marc, you're doing very impressively if this is the beginning of your Haskell career! Do feel free to keep asking here if you have more questions. On Mon, Apr 23, 2018 at 08:08:18PM +0200, Marc Busqué wrote:

...

Tom, thank you very much for your deep inspection. Your gist can be really helpful in trying to understand the problem. I will study it carefully. I have been reading books about Haskell and also Category Theory for some months, but I have just started coding few weeks ago, so I'm bit overwhelmed about having found a compiler bug so soon :D I'll look into all of this and also about Li-yao recommendations and if it is suitable I'll fill the issue and also report here.

Marc Busqué

2:49 p.m.

On Mon, 23 Apr 2018, Tom Ellis wrote:

...

Marc, you're doing very impressively if this is the beginning of your Haskell career! Do feel free to keep asking here if you have more questions.

Thanks for your encouragement :) Marc Busqué http://waiting-for-dev.github.io/about/

Li-yao Xia

7:58 a.m.

Hi Marc,

...

``` list :: (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table) ```

The only occurence of `s`/`s0` that is not ambiguous is between `select` and `query`, as the first argument of the data type `Query`. Everywhere else, there is a type family in the way which prevents unification; for example `Cols s a ~ Cols s0 a` does not imply `s ~ s0`. You can use a type annotation or TypeApplications to instantiate the `s0` between `query` and `select`. This requires ScopedTypeVariables, and an explicit `forall` at the top to make the type variables available in the definition body. Note that the type of `list` is also ambiguous for the aforementioned reasons, since `s` is only an argument of the type family `Res` (and `Cols`). You will have to AllowAmbiguousTypes to define it and write `list @s` (with TypeApplications) to use it. ``` {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-} list :: forall s a. (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table :: Query s _) -- or, ... (select @s table) -- with {-# LANGUAGE TypeApplications #-} ``` References in the GHC manual: - ScopedTypeVariables: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... - TypeApplications: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... - AllowAmbiguousTypes: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts... Li-yao

Marc Busqué

10:45 a.m.

On Mon, 23 Apr 2018, Li-yao Xia wrote:

...

Hi Marc,

...
``` list :: (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table) ```

The only occurence of `s`/`s0` that is not ambiguous is between `select` and `query`, as the first argument of the data type `Query`. Everywhere else, there is a type family in the way which prevents unification; for example `Cols s a ~ Cols s0 a` does not imply `s ~ s0`.

You can use a type annotation or TypeApplications to instantiate the `s0` between `query` and `select`. This requires ScopedTypeVariables, and an explicit `forall` at the top to make the type variables available in the definition body.

Note that the type of `list` is also ambiguous for the aforementioned reasons, since `s` is only an argument of the type family `Res` (and `Cols`). You will have to AllowAmbiguousTypes to define it and write `list @s` (with TypeApplications) to use it.

``` {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}

list :: forall s a. (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table :: Query s _) -- or, ... (select @s table) -- with {-# LANGUAGE TypeApplications #-} ```

References in the GHC manual:

- ScopedTypeVariables: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...

- TypeApplications: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...

- AllowAmbiguousTypes: https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts...

Li-yao

Thanks Li-yao. I'll studiy it thoroughly. It looks promising. Marc Busqué http://waiting-for-dev.github.io/about/

Marc Busqué

24 Apr 24 Apr

2 a.m.

Just for completeness about this solution: On Mon, 23 Apr 2018, Li-yao Xia wrote:

...

``` {-# LANGUAGE AllowAmbiguousTypes #-} {-# LANGUAGE ScopedTypeVariables #-}

list :: forall s a. (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] list table = withDB $ query (select table :: Query s _)

This gives error: ``` • Couldn't match type ‘Res a’ with ‘Res (Cols s a)’ Expected type: IO [Res (Cols s a)] Actual type: IO [Res a] NB: ‘Res’ is a type function, and may not be injective • In the expression: withDB $ query (select table :: Query s a) In an equation for ‘list’: list table = withDB $ query (select table :: Query s a) • Relevant bindings include table :: Table a (bound at src/Hedger/Backend.hs:30:6) list :: Table a -> IO [Res (Cols s a)] (bound at src/Hedger/Backend.hs:30:1) | 30 | list table = withDB $ query (select table :: Query s a) Couldn't match type ‘a’ with ‘Cols s a’ ‘a’ is a rigid type variable bound by the type signature for: list :: forall s a. (Result (Cols s a), Columns (Cols s a)) => Table a -> IO [Res (Cols s a)] at src/Hedger/Backend.hs:29:1-93 Expected type: Query s a Actual type: Query s (Cols s a) • In the first argument of ‘query’, namely ‘(select table :: Query s a)’ In the second argument of ‘($)’, namely ‘query (select table :: Query s a)’ In the expression: withDB $ query (select table :: Query s a) • Relevant bindings include table :: Table a (bound at src/Hedger/Backend.hs:30:6) list :: Table a -> IO [Res (Cols s a)] (bound at src/Hedger/Backend.hs:30:1) | 30 | list table = withDB $ query (select table :: Query s a) ```

...

-- or, ... (select @s table) -- with {-# LANGUAGE TypeApplications #-} ```

This indeed works!! In either case, however, I need to add `{-# LANGUAGE FlexibleContexts #-}` Now I have an interesting road in front of me in order to try to understand it, along with Tom Ellis' isolated reproducing environment :) Marc Busqué http://waiting-for-dev.github.io/about/

2583

Age (days ago)

2587

Last active (days ago)

List overview

Download

18 comments

4 participants

participants (4)

Brandon Allbery
Li-yao Xia
Marc Busqué
Tom Ellis

Selda: confused about type signtures

tags

participants (4)