bugfix in PGF.Type.pType: Agda style types like {x : A} -> B should not be supported in GF

1 files changed, 10 insertions, 15 deletions

diff --git a/src/runtime/haskell/PGF/Type.hs b/src/runtime/haskell/PGF/Type.hs
index e3cf46eec..b51b74a59 100644
--- a/src/runtime/haskell/PGF/Type.hs
+++ b/src/runtime/haskell/PGF/Type.hs
@@ -67,21 +67,16 @@ pType = do
       do (cat,args) <- pAtom

          return [(Explicit,wildCId,DTyp [] cat args)]

       RP.<++

-      (RP.between (RP.char '(') (RP.char ')') $ do

-         xs <- RP.option [(Explicit,wildCId)] $ do

-                     xs <- pBinds

-                     RP.skipSpaces

-                     RP.char ':'

-                     return xs

-         ty <- pType

-         return [(b,v,ty) | (b,v) <- xs])

-      RP.<++

-      (RP.between (RP.char '{') (RP.char '}') $ do

-         vs <- RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ',')

-         RP.skipSpaces

-         RP.char ':'

-         ty <- pType

-         return [(Implicit,v,ty) | v <- vs])

+      do RP.between (RP.char '(') (RP.char ')') pHypoBinds

+

+pHypoBinds = do

+   xs <- RP.option [(Explicit,wildCId)] $ do

+               xs <- pBinds

+               RP.skipSpaces

+               RP.char ':'

+               return xs

+   ty <- pType

+   return [(b,v,ty) | (b,v) <- xs]

 

     pAtom = do

       cat <- pCId