Re: [Haskell-cafe] Selda: confused about type signtures

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