Walk under constrained types during role inference

[kl0tl]

The Safe Zero-cost Coercions for Haskell paper argues that type instances arguments should get nominal roles in section 3.2 Preserving class coherence with the following exemple:

data HowToShow a where
  MkHTS :: Show a ⇒ HowToShow a

showH :: HowToShow a → a → String
showH MkHTS x = show x

instance Show HTML where
  show (MkHTML s) = "HTML:" ++ show s

stringShow :: HowToShow String
stringShow = MkHTS
htmlShow :: HowToShow HTML
htmlShow = MkHTS
badShow :: HowToShow HTML
badShow = coerce stringShow

λ> showH stringShow "Hello"
"Hello"
λ> showH htmlShow (MkHTML "Hello")
"HTML:Hello"
λ> showH badShow (MkHTML "Hello")
"Hello"

I can‘t think of a way to store an instance dictionary under a constructor in PureScript so we should be able to disregard the constraint arguments of constrained types entirely.

Fix #3868.

[kl0tl]

I’ve managed to reproduce the example in the paper with a foreign data type, but this rely on a lax role declaration and isn’t something that could be avoided by assigning nominal roles to the constraint arguments of constrained types.

module Example where

import Prelude

import Safe.Coerce (coerce)
import Unsafe.Coerce (unsafeCoerce)

foreign import data ShowDict :: Type -> Type
type role ShowDict representational

intro :: forall a. Show a => ShowDict a
intro = (unsafeCoerce :: (forall a. a -> a) -> (forall a. Show a => ShowDict a)) \dict -> dict

elim :: forall a b. (Show a => b) -> ShowDict a -> b
elim = unsafeCoerce ($)

withShowDict :: forall a. ShowDict a → a → String
withShowDict dict x = elim (show x) dict

newtype HTML = MkHTML String
instance showHTML :: Show HTML where
  show (MkHTML s) = "HTML:" <> show s

showStringDict :: ShowDict String
showStringDict = intro

showHTMLDict :: ShowDict HTML
showHTMLDict = intro

badShowDict :: ShowDict HTML
badShowDict = coerce showStringDict

> import Example
> withShowDict showStringDict "Hello"
"\"Hello\""

> withShowDict showHTMLDict (MkHTML "Hello")
"HTML:\"Hello\""

> withShowDict badShowDict (MkHTML "Hello")
"\"Hello\""

[kl0tl]

I’ve found a reason to assign at least a representational role to the constraint arguments of constrained types!

Not considering the constraint of constrained types at all when inferring roles allows to provide arbitrary dictionaries:

module Example where

import Prelude

import Safe.Coerce (coerce)

newtype Shown a = Shown (Show a => String)

shownUnit :: Shown Unit
shownUnit = Shown $ show unit

example :: String
example = case (coerce :: Shown Unit -> Shown Ordering) shownUnit of
  Shown shown -> shown

Which can lead to runtime exceptions:

…/output/Data.Ordering/index.js:37
    throw new Error("Failed pattern match at Data.Ordering (line 26, column 1 - line 29, column 17): " + [ v.constructor.name ]);
    ^

Error: Failed pattern match at Data.Ordering (line 26, column 1 - line 29, column 17): Object
    at …/output/Data.Ordering/index.js:37:11
    at …/output/Example/index.js:11:36
    at …/output/Example/index.js:15:12
    at Object.<anonymous> (…/output/Example/index.js:16:3)

The newtype is necessary here because we don’t solve constraints for constrained types in general, so coerce :: (Show Unit => String) -> Show Ordering => String is rejected with the following error:

  No type class instance was found for
                                                   
    Prim.Coerce.Coercible (Show Unit => String)    
                          (Show Ordering => String)
                                                   

while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
  is at least as general as type (Show Unit => String) -> (Show Ordering => String)
while checking that expression coerce
  has type (Show Unit => String) -> (Show Ordering => String)

[hdgarrood]

I feel like things appearing as parameters to constraints under data constructors should probably be nominal, but I’ll need to reread the relevant part of the paper to be sure.

[kl0tl]

The paper doesn’t mention constraints under data constructors in section 4.5 Role inference but given how they desugar I think we ought to walk the members of the type class.

This doesn’t break type classes coherence and it’s enough to reject unsafe coercions:

module Example where

import Prelude

import Data.Ord.Down (Down)
import Data.Set (Set)
import Data.Set as Set
import Effect (Effect)
import Effect.Console (log)
import Safe.Coerce (coerce)

newtype Shown a = Shown (Show a => String)

class Insert a where
  insert :: a -> Set a -> Set a

instance insertOrd :: Ord a => Insert a where
  insert = Set.insert

newtype Inserted a b = Inserted (Insert a => b)

insertedInt :: Inserted Int (Shown (Set Int))
insertedInt = Inserted $ Shown $ show $ insert 0 $ Set.fromFoldable [1, 2]

main :: Effect Unit
main = case (coerce :: Inserted Int (Shown (Set Int)) -> Inserted (Down Int) (Shown (Set (Down Int)))) insertedInt of
  Inserted inserted -> case inserted of
    Shown shown -> log shown

Error found:
in module Example
at Example.purs:26:14 - 26:20 (line 26, column 14 - line 26, column 20)

  No type class instance was found for
                                                                        
    Prim.Coerce.Coercible (Inserted Int (Shown (Set Int)))              
                          (Inserted (Down Int) (Shown (Set (Down Int))))
                                                                        

while checking that type forall (a :: Type) (b :: Type). Coercible a b => a -> b
  is at least as general as type Inserted Int (Shown (Set Int)) -> Inserted (Down Int) (Shown (Set ...))
while checking that expression coerce
  has type Inserted Int (Shown (Set Int)) -> Inserted (Down Int) (Shown (Set ...))
in value declaration main

See https://github.com/purescript/documentation/blob/master/errors/NoInstanceFound.md for more information,
or to contribute content related to this error.

Given a type role Set nominal declaration, inferring any role more permissive than nominal for the first parameter of Inserted would let this program compile and log:

> node -e 'require("./output/Example").main()'
(fromFoldable ((Down 1) : (Down 2) : (Down 0) : Nil))

Which is rather unexpected for a Set (Down Int)!

[kl0tl]

I’ve managed to capture a dictionary under a newtype!

module Example where

import Prelude

import Safe.Coerce (coerce)

newtype Shown a = Shown ((Show a => a -> String) -> String)

shown :: forall a. Shown a -> String
shown = case _ of
  Shown f -> f show

newtype HTML = MkHTML String
instance showHTML :: Show HTML where
  show (MkHTML s) = "HTML:" <> show s

shownString :: Shown String
shownString = Shown (\f -> f "Hello")

shownHTML :: Shown HTML
shownHTML = Shown (\f -> f (MkHTML "Hello"))

badShownHTML :: Shown HTML
badShownHTML = coerce shownString

> import Example
> shown shownString
"\"Hello\""

> shown shownHTML
"HTML:\"Hello\""

> shown badShownHTML
"\"Hello\""

Anything more permissive than nominal breaks coherence after all 🙈

[hdgarrood]

The code all looks good, but I think it would be worth adding a test where a type variable mentioned in a constraint is shadowing one of the type parameters (as I don't think we have one already). For example, I think this should be accepted:

class C a

data Test a = Test a (forall a. C a => a)

type role Test representational

[kl0tl]

You’re right, we ought to ensure we don’t assign nominal roles to parameters shadowed by locally bound variables. I added a the test you suggested.

[hdgarrood]

Thanks!

[hdgarrood]

Would you mind merging master here to see if CI passes too?

[kl0tl]

I rebased on top of master, tests pass again 😌

[hdgarrood]

🎉