more roles work

roles/Main.hs

@@ -1,4 +1,5 @@
 {-# LANGUAGE Trustworthy #-}
+{-# LANGUAGE StandaloneDeriving #-}
 module Main where
 
 import Data.Coerce
@@ -9,6 +10,11 @@ newtype MyInt = MyInt Int deriving (Eq, Show)
 instance Ord MyInt where
   (MyInt x) <= (MyInt y) = y <= x
 
+-- class IntIso t where
+--     intIso :: Set t -> Set Int
+--
+-- deriving instance IntIso MInt
+
 main :: IO ()
 main =
   let ints     = [1,3,5,2] :: [Int]

roles2/ExpDicts.hs

@@ -0,0 +1,33 @@
+{-# LANGUAGE GADTs #-}
+module Main where
+
+import Data.Coerce
+
+import ExpDicts_Sub
+
+data C a where
+  C :: MEQ a => C a
+
+newtype CChar = CChar Char
+
+instance MEQ CChar where
+  meq _ _ = False
+
+dictChar :: C Char
+dictChar = C
+
+dictCChar :: C CChar
+dictCChar = C
+
+dictChar' :: C Char
+dictChar' = coerce dictCChar
+
+expMEQ :: C a -> a -> a -> Bool
+expMEQ C a b = a `meq` b
+
+main :: IO ()
+main = do
+  print $ expMEQ dictChar  'a' 'a'
+  print $ expMEQ dictCChar  (CChar 'a') (CChar 'a')
+  print $ expMEQ dictChar' 'a' 'a'
+

roles2/ExpDicts_Sub.hs

@@ -0,0 +1,16 @@
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE IncoherentInstances #-}
+module ExpDicts_Sub (
+    MEQ(..),
+    normMEQ
+  ) where
+
+-- Requires we explicitly use representational
+type role MEQ representational
+class MEQ a where { meq :: a -> a -> Bool }
+
+instance MEQ Char where { meq _ _ = True }
+
+normMEQ :: MEQ a => a -> a -> Bool
+normMEQ a b = a `meq` b
+

roles2/README.md

@@ -0,0 +1,12 @@
+# GND & Roles
+
+Another test of roles. See `roles` folder for a description of roles and their
+interaction with Safe Haskell.
+
+Here we test typeclasses, and ensure that since they are nominal by default,
+without explicit annotations abstract boundaries can't be broken.
+
+## Result
+
+Safe.
+

roles2/RolesClasses.hs

@@ -0,0 +1,57 @@
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE RoleAnnotations #-}
+{-# LANGUAGE IncoherentInstances #-}
+{-# LANGUAGE GeneralizedNewtypeDeriving #-}
+{-# LANGUAGE StandaloneDeriving #-}
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE FlexibleContexts #-}
+module RolesClasses where
+
+import Data.Coerce
+
+-- ===============================================
+-- Can I Coerce dictionaries?
+--
+
+-- Can't do! Can't lower from nominal which comes about as `Eq a` is nominal.
+-- type role Foo representational
+data Foo a where
+  Foo :: Eq a => Foo a
+
+newtype Bar = Bar Int
+instance Eq Bar where
+  _ == _ = False
+
+
+-- ===============================================
+-- Coerce a newtype
+
+newtype Car a = Car a
+type Car' = Car Int
+
+-- Can coerce newtype since constructor in scope and default is
+-- representational
+cast1 = coerce (1 :: Int) :: Car'
+
+
+-- Can coerce since `B a` is representational by default
+data B a where { B :: B a }
+cast2 = coerce (B :: B Int) :: B Car'
+
+-- Can't do since Foo a is nominal
+-- cast = coerce (Foo :: Foo Int) :: Foo Bar
+
+
+-- Can derive MEQ a (so a is behaving as representational)
+-- i.e., MEQ Int -> MEQ Car
+class MEQ a where { meq :: a -> a -> Bool }
+instance MEQ Int where { meq a b = a == b }
+deriving instance MEQ Car'
+
+-- Only works when we reduce `MEQ a` to be representational from the default
+-- nominal setting, as otherwise `A a` is also required to be nominal due to
+-- the MEQ constraint.
+type role MEQ representational
+data A a where { A :: MEQ a => A a }
+cast4 = coerce (A :: A Int) :: A Car'
+