Comments for 2019-03-16

[rcook]

No description provided.

[mgsloan]

GHC bug about quantified contexts + commutativity of coercible: https://gitlab.haskell.org/ghc/ghc/issues/16432

Ryan GI Scott's blog about how quantified contexts can make it possible to have join in the monad class while still being able to use generalized newtype deriving: https://ryanglscott.github.io/2018/03/04/how-quantifiedconstraints-can-let-us-put-join-back-in-monad/

10 months ago I put up my idea for making coercible know that the same instances are used for different newtypes - https://www.reddit.com/r/haskell/comments/8h2lon/could_coercible_be_extended_to_work_on/ . An interesting point that Richerd Eisenberg made in the comments is that Coercible (Hashable a) (Hashable a') would be misleading since dictionaries for the same class should always have the same representation. So that's why it makes more sense to name it something more like SameDict or so

[mgsloan]

Also, I made a claim that

f :: (a ~ b, b ~ c) => a -> c
f = id

Doesn't typecheck. I was wrong! Transitivity actually does work for type equality. Curiously, this doesn't work directly for Coercible:

{-# LANGUAGE GADTs #-}
import Data.Coerce

f :: (Coercible a b, Coercible b c) => a -> c
f = coerce

Results in

hmm.hs:4:6: error:                                                                      
    • Couldn't match representation of type ‘b0’ with that of ‘c’                       
      ‘c’ is a rigid type variable bound by                                             
        the type signature for:                                                         
          f :: forall a b c. (Coercible a b, Coercible b c) => a -> c                   
        at hmm.hs:4:6-45                                                                
    • In the ambiguity check for ‘f’                                                    
      To defer the ambiguity check to use sites, enable AllowAmbiguousTypes
      In the type signature:                                                            
        f :: (Coercible a b, Coercible b c) => a -> c                                   
  |
4 | f :: (Coercible a b, Coercible b c) => a -> c

But this can be resolved by doing

{-# LANGUAGE GADTs #-}
import Data.Coerce
import Data.Proxy

f :: (Coercible a b, Coercible b c) => Proxy b -> a -> c
f _ = coerce

The ambiguity is resolved by the caller specifying the intermediate type to coerce through.

It's curious that this ambiguity is an issue for Coercible but not for type equality.

Once place where things get squirrely for transitivity of Coercible is described here:

f :: (Coercible (a b) (c d), Coercible (c d) (e f)) => Proxy (c d) -> a b -> e f
f _ = coerce

Yields error:

hmm.hs:8:7: error:                                                                      
    • Couldn't match representation of type ‘a b’ with that of ‘e f’                    
        arising from a use of ‘coerce’                                                  
    • In the expression: coerce                                                         
      In an equation for ‘f’: f _ = coerce                                              
    • Relevant bindings include                                                         
        f :: Proxy (c d) -> a b -> e f (bound at hmm.hs:8:1)                            
  |                                                                                     
8 | f _ = coerce