[Agda] Pattern matching on irrelevant types with only one constructor?

[Thorsten Altenkirch]

That is not really an argument.

Clearly there are many situations where we would like to reduce a term which will only terminate in a consistent context. E.g. we can reduce terms which are only guarded by a proof of well-foundedness. Another situation is wether you can reduce a coercion which relies on an equality proof. The latter could lead to a failure of type-soundness but does it matter when we execute symbolically (i.e. not at run-time).

I don't say that the answer is always that we shouldn't care, but I was asking for better arguments why we should.

Thorsten

On 01/05/2019, 15:35, "Agda on behalf of Jon Sterling" <agda-bounces at lists.chalmers.se on behalf of jon at jonmsterling.com> wrote:

    To respond to Thorsten's comments a bit further down the thread, I tried really hard to make proof assistants without a complete decision procedure for typing practical, and I determined that it is not likely to work out. Decidable type checking is good.
    
    




This message and any attachment are intended solely for the addressee
and may contain confidential information. If you have received this
message in error, please contact the sender and delete the email and
attachment. 

Any views or opinions expressed by the author of this email do not
necessarily reflect the views of the University of Nottingham. Email
communications with the University of Nottingham may be monitored 
where permitted by law.