cba27c8 · Idris-dev · git.iko.soy

src/Idris/Core/Elaborate.hs+3−1

@@ -732,7 +732,9 @@ apply_elab n args =

732checkPiGoal :: Name -> Elab' aux ()

733checkPiGoal n

734 = do g <- goal

735+ ctxt <- get_context

736+ env <- get_env

735− case g of

737+ case (normalise ctxt env g) of

736 Bind _ (Pi _ _ _) _ -> return ()

738 Bind _ (Pi _ _ _) _ -> return ()

737 _ -> do a <- getNameFrom (sMN 0 "__pargTy")

739 _ -> do a <- getNameFrom (sMN 0 "__pargTy")

738 b <- getNameFrom (sMN 0 "__pretTy")

740 b <- getNameFrom (sMN 0 "__pretTy")

test/basic012/basic012a.idrnew file+10

@@ -0,0 +1,10 @@

1+Symmetric : {c : Type} -> (c -> c -> Type) -> Type

2+Symmetric {c} rel = {a : c} -> {b : c} -> rel a b -> rel b a

3+

4+record Symmetry (t : Type) (rel : t -> t -> Type) where

5+ constructor MkSymmetry

6+ is_symmetric : Symmetric {c=t} rel

7+

8+symmetry : {ty : Type} -> Symmetry ty (=)

9+symmetry = MkSymmetry sym

10+

test/basic012/run+1

@@ -1,4 +1,5 @@

1#!/usr/bin/env bash

2${IDRIS:-idris} $@ basic012.idr -o basic012

3./basic012

4+${IDRIS:-idris} $@ basic012a.idr --check

4rm -f basic012 *.ibc

5rm -f basic012 *.ibc