Support for equality constraints

src/Agda2Hs/Compile/Data.hs

@@ -18,7 +18,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.AgdaUtils
 
 import Agda2Hs.Compile.Name
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 

src/Agda2Hs/Compile/Function.hs

@@ -38,7 +38,7 @@ import Agda.Utils.Size ( Sized(size) )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName )
 import Agda2Hs.Compile.Term ( compileTerm, usableDom, dependentDom )
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileDomType )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileDomType )
 import Agda2Hs.Compile.TypeDefinition ( compileTypeDef )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
@@ -257,6 +257,7 @@ keepClause c@Clause{..} = case (clauseBody, clauseType) of
   (Just body, Just cty) -> compileDom (domFromArg cty) <&> \case
     DODropped  -> False
     DOInstance -> True
+    DOEquality -> True
     DOType     -> __IMPOSSIBLE__
     DOTerm     -> True
 
@@ -301,6 +302,7 @@ compilePats ty ((namedArg -> pat):ps) = do
   let rest = compilePats (absApp b (patternToTerm pat)) ps
   compileDom a >>= \case
     DOInstance -> rest
+    DOEquality -> rest
     DODropped  -> rest
     DOType     -> rest
     DOTerm     -> do

src/Agda2Hs/Compile/Record.hs

@@ -24,7 +24,7 @@ import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.ClassInstance
 import Agda2Hs.Compile.Function ( compileFun )
-import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom, DomOutput(..) )
+import Agda2Hs.Compile.Type ( compileDomType, compileTeleBinds, compileDom )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 

src/Agda2Hs/Compile/Term.hs

@@ -41,7 +41,7 @@ import Agda.Utils.Size
 import Agda2Hs.AgdaUtils
 import Agda2Hs.Compile.Name ( compileQName, importInstance )
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTelSize, compileDomType )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileTelSize, compileDomType )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )
@@ -508,6 +508,7 @@ dependentDom dom = do
     DOTerm     -> False
     DOInstance -> False
     DODropped  -> False
+    DOEquality -> False
 
 compileLam :: Type -> ArgInfo -> Abs Term -> C (Hs.Exp ())
 compileLam ty argi abs = do
@@ -612,6 +613,7 @@ compileArgs' ty (x:xs) = do
   compileDom a >>= \case
     DODropped  -> rest
     DOInstance -> checkInstance x *> rest
+    DOEquality -> checkInstance x *> rest
     DOType     -> checkValidType x *> rest
     DOTerm     -> second . (:) <$> compileTerm (unDom a) x <*> rest
 
@@ -653,7 +655,8 @@ checkInstance u = do
     Con c _ _
       | prettyShow (conName c) == "Agda.Builtin.Unit.tt" ||
         prettyShow (conName c) == "Haskell.Prim.IsTrue.itsTrue" ||
-        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" -> return ()
+        prettyShow (conName c) == "Haskell.Prim.IsFalse.itsFalse" ||
+        prettyShow (conName c) == "Agda.Builtin.Equality.refl" -> return ()
     _ -> illegalInstance
 
   where

src/Agda2Hs/Compile/Type.hs

@@ -101,6 +101,7 @@ compileType t = do
         DomType _ hsA -> Hs.TyFun () hsA <$> compileB
         DomConstraint hsA -> constrainType hsA <$> compileB
         DomDropped -> compileB
+        DomEquality hsA -> constrainType hsA <$> compileB
         DomForall Nothing -> compileB
         DomForall (Just hsA) -> qualifyType hsA <$> compileB
 
@@ -173,6 +174,7 @@ compileTel (ExtendTel a tel) = compileDom a >>= \case
   DOInstance -> __IMPOSSIBLE__
   DOType     -> __IMPOSSIBLE__
   DOTerm     -> (:) <$> compileType (unEl $ unDom a) <*> underAbstraction a tel compileTel
+  DOEquality -> __IMPOSSIBLE__
 
 -- Version of @compileTel@ that just computes the size,
 -- and avoids compiling the types themselves.
@@ -183,6 +185,7 @@ compileTelSize (ExtendTel a tel) = compileDom a >>= \case
   DOInstance -> __IMPOSSIBLE__
   DOType -> __IMPOSSIBLE__
   DOTerm -> (1+) <$> underAbstraction a tel compileTelSize
+  DOEquality -> __IMPOSSIBLE__
 
 compileUnboxType :: QName -> Args -> C (Hs.Type ())
 compileUnboxType r pars = do
@@ -205,19 +208,18 @@ compileTransparentType ty args = compileTypeArgs ty args >>= \case
   (v:vs) -> return $ v `tApp` vs
   []     -> __IMPOSSIBLE__
 
-
-data DomOutput = DOInstance | DODropped | DOType | DOTerm
-
 compileDom :: Dom Type -> C DomOutput
 compileDom a = do
   isErasable <- pure (not $ usableModality a) `or2M` canErase (unDom a)
   isClassConstraint <- pure (isInstance a) `and2M` isClassType (unDom a)
+  isEqualityConstraint <- pure (usableModality a) `and2M` pure (isInstance a) `and2M` isBuiltinEqualityType (unDom a)
   isType <- endsInSort (unDom a)
   return $ if
-    | isErasable        -> DODropped
-    | isClassConstraint -> DOInstance
-    | isType            -> DOType
-    | otherwise         -> DOTerm
+    | isEqualityConstraint -> DOEquality
+    | isClassConstraint  -> DOInstance
+    | isErasable         -> DODropped
+    | isType             -> DOType
+    | otherwise          -> DOTerm
 
 -- | Compile a function type domain.
 -- A domain can either be:
@@ -231,6 +233,7 @@ compileDomType x a =
   compileDom a >>= \case
     DODropped  -> pure DomDropped
     DOInstance -> DomConstraint . Hs.TypeA () <$> compileType (unEl $ unDom a)
+    DOEquality -> compileEqualityConstraint (unEl $ unDom a)
     DOType     -> do
       -- We compile (non-erased) type parameters to an explicit forall if they
       -- come from a module parameter or if we are in a nested position inside the type.
@@ -250,6 +253,16 @@ compileDomType x a =
         | otherwise -> return $ DomForall Nothing
     DOTerm     -> fmap (uncurry DomType) . withNestedType . compileTypeWithStrictness . unEl $ unDom a
 
+compileEqualityConstraint :: Term -> C CompiledDom
+compileEqualityConstraint t = do
+  Def _ es <- reduce t
+  -- The arguments to equality are _a_ (level), _A_ (the type of elements), x (: A), and y (: A)
+  -- We want to compile x and y
+  let Just (_:_:x:y:_) = allApplyElims es
+  hsX <- compileType (unArg x)
+  hsY <- compileType (unArg y)
+  return $ DomEquality $ Hs.TypeA () $ Hs.TyInfix () hsX (Hs.UnpromotedName () (Hs.UnQual () (Hs.Symbol () "~"))) hsY
+
 compileTeleBinds :: Bool -> Telescope -> C [Hs.TyVarBind ()]
 compileTeleBinds kinded = go
   where
@@ -264,6 +277,7 @@ compileTeleBinds kinded = go
         (ha:) <$> underAbstraction a tel go
       DOInstance -> agda2hsError "Constraint in type parameter not supported"
       DOTerm -> agda2hsError "Term variable in type parameter not supported"
+      DOEquality -> agda2hsError "Equality constraint in type parameter not supported"
 
 compileKeptTeleBind :: Bool -> Hs.Name () -> Type -> C (Hs.TyVarBind ())
 compileKeptTeleBind kinded x t = do

src/Agda2Hs/Compile/TypeDefinition.hs

@@ -15,7 +15,7 @@ import Agda.TypeChecking.Telescope ( mustBePi )
 import Agda.Utils.Impossible ( __IMPOSSIBLE__ )
 import Agda.Utils.Monad
 
-import Agda2Hs.Compile.Type ( compileType, compileDom, DomOutput(..), compileTypeArgs )
+import Agda2Hs.Compile.Type ( compileType, compileDom, compileTypeArgs )
 import Agda2Hs.Compile.Types
 import Agda2Hs.Compile.Utils
 import Agda2Hs.Compile.Var ( compileDBVar )

src/Agda2Hs/Compile/Types.hs

@@ -197,8 +197,10 @@ instance Null a => Null (C a) where
   null = __IMPOSSIBLE__
 instance Semigroup a => Semigroup (C a) where (<>) = liftA2 (<>)
 
+-- | Determines how a 'Dom Type' is treated during compilation.
+data DomOutput = DODropped | DOInstance | DOType | DOTerm | DOEquality
 
-
+-- | Determines how an argument is compiled.
 -- | Agda @Dom Type@ can get compiled in three ways.
 data CompiledDom
   = DomType Strictness (Hs.Type ())
@@ -209,6 +211,9 @@ data CompiledDom
     -- ^ To a forall, with an optional type variable declaration. If Nothing, this is an implicit forall; otherwise, explicit.
   | DomDropped
     -- ^ To nothing (e.g. erased proofs)
+  | DomEquality (Hs.Asst ())
+    -- ^ To an equality constraint (e.g. `(a ~ b)`)
+
 
 -- | Whether a datatype/record should be compiled as a @newtype@ haskell definition.
 type AsNewType = Bool

src/Agda2Hs/Compile/Utils.hs

@@ -233,6 +233,16 @@ isClassType a = do
     Def cl _ -> isClassName cl
     _        -> return False
 
+-- | Check if the given type corresponds to the Agda built-in equality.
+isBuiltinEqualityType :: Type -> C Bool
+isBuiltinEqualityType a = do
+  TelV _ t <- telView a
+  case unEl t of
+    Def f _ -> do
+      name <- getBuiltinName' builtinEquality
+      return $ Just f == name
+    _ -> return False
+
 -- Drops the last (record) module for typeclass methods
 dropClassModule :: ModuleName -> C ModuleName
 dropClassModule m@(MName ns) = isClassModule m >>= \case

test/Succeed/EqualityConstraint.agda

@@ -0,0 +1,8 @@
+module EqualityConstraint where
+
+open import Haskell.Prelude
+
+postulate
+  myFunc : ⦃ p : a ≡ b ⦄ → c
+
+{-# COMPILE AGDA2HS myFunc #-}

test/Succeed/EqualityConstraint.hs

@@ -0,0 +1,6 @@
+{-# LANGUAGE TypeOperators #-}
+module EqualityConstraint where
+
+myFunc :: a ~ b => c
+myFunc = error "postulate:   a ~ b => c"
+