Add coerce primitive

Use `unsafeCoerce` when there is an (erased) proof that types are identical.

Fixes: #135

lib/Haskell/Prelude.agda

@@ -135,3 +135,8 @@ xs !! n = xs !!ᴺ intToNat n
 lookup : ⦃ Eq a ⦄ → a → List (a × b) → Maybe b
 lookup x []              = Nothing
 lookup x ((x₁ , y) ∷ xs) = if x == x₁ then Just y else lookup x xs
+
+private variable A B : Set
+
+coerce : @0 A ≡ B → A → B
+coerce refl x = x

src/Agda2Hs/Compile/Name.hs

@@ -61,16 +61,17 @@ toNameImport x (Just mod) =
 -- | Default rewrite rules.
 defaultSpecialRules :: SpecialRules
 defaultSpecialRules = Map.fromList
-  [ "Agda.Builtin.Nat.Nat"          `to` "Natural" `importing` Just "Numeric.Natural"
-  , "Haskell.Control.Monad.guard"   `to` "guard"   `importing` Just "Control.Monad"
-  , "Agda.Builtin.Int.Int"          `to` "Integer" `importing` Nothing
-  , "Agda.Builtin.Word.Word64"      `to` "Word"    `importing` Nothing
-  , "Agda.Builtin.Float.Float"      `to` "Double"  `importing` Nothing
-  , "Agda.Builtin.Bool.Bool.false"  `to` "False"   `importing` Nothing
-  , "Agda.Builtin.Bool.Bool.true"   `to` "True"    `importing` Nothing
-  , "Haskell.Prim._∘_"              `to` "_._"     `importing` Nothing
-  , "Haskell.Prim.Monad.Dont._>>=_" `to` "_>>=_"   `importing` Nothing
-  , "Haskell.Prim.Monad.Dont._>>_"  `to` "_>>_"    `importing` Nothing
+  [ "Agda.Builtin.Nat.Nat"          `to` "Natural"      `importing` Just "Numeric.Natural"
+  , "Haskell.Control.Monad.guard"   `to` "guard"        `importing` Just "Control.Monad"
+  , "Haskell.Prelude.coerce"        `to` "unsafeCoerce" `importing` Just "Unsafe.Coerce"
+  , "Agda.Builtin.Int.Int"          `to` "Integer"      `importing` Nothing
+  , "Agda.Builtin.Word.Word64"      `to` "Word"         `importing` Nothing
+  , "Agda.Builtin.Float.Float"      `to` "Double"       `importing` Nothing
+  , "Agda.Builtin.Bool.Bool.false"  `to` "False"        `importing` Nothing
+  , "Agda.Builtin.Bool.Bool.true"   `to` "True"         `importing` Nothing
+  , "Haskell.Prim._∘_"              `to` "_._"          `importing` Nothing
+  , "Haskell.Prim.Monad.Dont._>>=_" `to` "_>>=_"        `importing` Nothing
+  , "Haskell.Prim.Monad.Dont._>>_"  `to` "_>>_"         `importing` Nothing
   ]
   where infixr 6 `to`, `importing`
         to = (,)

test/AllTests.agda

@@ -62,6 +62,7 @@ import Issue169
 import Issue210
 import ModuleParameters
 import ModuleParametersImports
+import Coerce
 
 {-# FOREIGN AGDA2HS
 import Issue14
@@ -124,4 +125,5 @@ import Issue169
 import Issue210
 import ModuleParameters
 import ModuleParametersImports
+import Coerce
 #-}

test/Coerce.agda

@@ -0,0 +1,16 @@
+open import Haskell.Prelude
+
+data A : Set where
+  MkA : Nat → A
+
+data B : Set where
+  MkB : Nat → B
+
+postulate A≡B : A ≡ B
+
+coerceExample : B
+coerceExample = coerce A≡B (MkA 5)
+
+{-# COMPILE AGDA2HS A newtype #-}
+{-# COMPILE AGDA2HS B newtype deriving (Show) #-}
+{-# COMPILE AGDA2HS coerceExample #-}

test/Fail/Issue142.agda

@@ -2,6 +2,7 @@ module Fail.Issue142 where
 
 open import Haskell.Prelude
 
-coerce : @0 a ≡ b → a → b
-coerce refl x = x
-{-# COMPILE AGDA2HS coerce #-}
+-- `coerce` is a primitive but this general structure remains disallowed
+falseCoerce : @0 a ≡ b → a → b
+falseCoerce refl x = x
+{-# COMPILE AGDA2HS falseCoerce #-}

test/golden/AllTests.hs

@@ -60,4 +60,5 @@ import Issue169
 import Issue210
 import ModuleParameters
 import ModuleParametersImports
+import Coerce
 

test/golden/Coerce.hs

@@ -0,0 +1,13 @@
+module Coerce where
+
+import Numeric.Natural (Natural)
+import Unsafe.Coerce (unsafeCoerce)
+
+newtype A = MkA Natural
+
+newtype B = MkB Natural
+              deriving (Show)
+
+coerceExample :: B
+coerceExample = unsafeCoerce (MkA 5)
+

test/golden/Issue142.err

@@ -1,2 +1,2 @@
-test/Fail/Issue142.agda:5,1-7
+test/Fail/Issue142.agda:6,1-12
 not supported by agda2hs: forced (dot) patterns in non-erased positions