Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Unexpected behavior of coerce inside foldMap's callback

Tags:

haskell

coerce

This code compiles:

import Data.List (isPrefixOf)
import Data.Monoid (Any(..))
import Data.Coerce

isRoot :: String -> Bool
isRoot path = getAny $ foldMap (coerce . isPrefixOf) ["src", "lib"] $ path

I'm using coerce as a shortcut for wrapping the final result of isPrefixOf in Any.

This similar code doesn't compile (notice the lack of .):

isRoot :: String -> Bool
isRoot path = getAny $ foldMap (coerce isPrefixOf) ["src", "lib"] $ path

The error is:

* Couldn't match representation of type `a0' with that of `Char'
    arising from a use of `coerce'
* In the first argument of `foldMap', namely `(coerce isPrefixOf)'
  In the first argument of `($)', namely
    `foldMap (coerce isPrefixOf) ["src", "lib"]'
  In the second argument of `($)', namely
    `foldMap (coerce isPrefixOf) ["src", "lib"] $ path'

But my intuition was that it, too, should compile. After all, we know that the arguments of isPrefixOf will be Strings, and that the result must be of typeAny. There's no ambiguity. So String -> String -> Bool should be converted to String -> String -> Any. Why isn't it working?

like image 356
danidiaz Avatar asked Dec 30 '22 14:12

danidiaz


2 Answers

This doesn't really have anything to do with coercions. It's just constraint solving in general. Consider:

class Foo a b
instance Foo (String -> Bool) (String -> Any)
instance Foo (String -> String -> Bool) (String -> String -> Any)

foo :: Foo a b => a -> b
foo = undefined

bar :: String -> String -> Any
bar = foo . isPrefixOf

baz :: String -> String -> Any
baz = foo isPrefixOf

The definition of bar works fine; the definition of baz fails.

In bar, the type of isPrefixOf can be directly inferred as String -> String -> Bool, simply by unifying the type of bars first argument (namely String) with the first argument type of isPrefixOf.

In baz, nothing whatsoever can be inferred about the type of isPrefixOf from the expression foo isPrefixOf. The function foo could do anything to the type of isPrefix to get the resulting type String -> String -> Any.

Remember that constraints don't really influence type unification. Unification occurs as if the constraints weren't there, and when unification is finished, the constraints are demanded.

Getting back to your original example, the following is a perfectly valid coercion, so the ambiguity is real:

{-# LANGUAGE TypeApplications #-}

import Data.Char
import Data.List (isPrefixOf)
import Data.Monoid (Any(..))
import Data.Coerce

newtype CaselessChar = CaselessChar Char
instance Eq CaselessChar where CaselessChar x == CaselessChar y = toUpper x == toUpper y

isRoot :: String -> Bool
isRoot path = getAny $ foldMap (coerce (isPrefixOf @CaselessChar)) ["src", "lib"] $ path
like image 111
K. A. Buhr Avatar answered Jan 06 '23 03:01

K. A. Buhr


isPrefix has inferred type [a] -> [a] -> Bool (with a constraint Eq a) the expected type of coerce isPrefix there is [Char] -> [Char] -> Any, so you end up with a constraint Coercible a Char, but there is nothing that actually constrains a to be Char. In fact, it could be any newtype around Char, which might have a different Eq instance.

newtype CChar = CChar Char

instance Eq CChar where
  _ == _ = True

bad :: String -> Bool
bad path = getAny $ foldMap (coerce (isPrefixOf :: [CChar] -> [CChar] -> Bool)) ["src", "lib"] $ path
like image 29
Li-yao Xia Avatar answered Jan 06 '23 04:01

Li-yao Xia