[Agda] new option -no-injectivity-check

[Makoto Takeyama]

Hi Ulf,

I also uploaded another patch that disables injectivity checking to

http://appserv.cs.chalmers.se/users/ulfn/wiki/agda.php?n=Patch.Submitted

With the pragma option --no-injectivity-check, everything is regarded as
NotInjective.

I needed this to typecheck our program that tries to primPutStr a
string expression, which becomes 1M byte long _if evaluated_.  But
Typechecking.Injectivity.checkInjectivity seems to reduce the right
hand side of a definition during type checking and Agda died on us
on the said program.  Without injectivity checking, Agda type
checked it fine.

Best Wishes,

Makoto

-- 
Makoto Takeyama <makoto.takeyama at aist.go.jp>
AIST/CVS (National Institute of Advanced Industrial Science and Technology /
          Research Center for Verification and Semantics)
tel: +81-6-4863-5019   fax: +81-6-4863-5052