[Haskell-cafe] Two mysteries

[Tom Ellis]

On Sun, Aug 28, 2022 at 09:36:56AM -0700, Henry Laxen wrote:
> class State a  where
>   type StateKey   a :: *
>   type StateValue a :: *
>   lensTmap          :: Functor f => Lenstype f a (TMap (StateKey a) (StateValue a))
>   lensKey           :: Functor f => Lenstype f a (StateKey a)
>   lensCounter       :: Functor f => Lenstype f (StateValue a) Int
> 
> updateState state f = liftIO $ do
>   let
>     key      = state ^. lensKey   -- read the key
>     mutable  = state ^. lensTmap  -- find the TVar of the TMap
>   withKey key (\(Just x) -> x & lensCounter %~ f) mutable -- update it
> 
> -- THE FIRST MYSTERY: If I use the inferred type explicitly for updateState
> -- above, this no longer compiles.  I get a "could not deduce" error
> -- reproduced below:
> 
> -- xupdateState
> --   :: (MonadIO m, Ord (StateKey s), State s, State a,
> --       StateValue s ~ StateValue a) =>
> --      s -> (Int -> Int) -> m ()
> -- xupdateState state f = liftIO $ do
> --   let
> --     key      = state ^. lensKey   -- read the key
> --     mutable  = state ^. lensTmap  -- find the TVar of the TMap
> --   withKey key (\(Just x) -> x & lensCounter %~ f) mutable -- update it

AllowAmbiguousTypes is what's allowing you to get tangled into this
knot.  I suggest you don't enable that extension unless you feel
confident you are equipped for axe warfare.

The behaviour here is as though the type checker has turned
`lensCounter` in the body into `lensCounter @a` for a fresh type
variable `a`, and then applied the necessary constraints to the
context.  Normally the type checker would notice that `a` is ambiguous
and refuse to continue.  AllowAmbiguousTypes defers that check to the
use site.  That means I don't think it makes any difference to you,
because even though `updateState` with inferred type signature will
compile I bet you can't use it.  Give it a try!  I guess you'll get an
"ambiguous type" error at the use site.

Tom