coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] "Cannot satisfy constraint" error using subset types

From: Klaus Ostermann <klaus.ostermann AT uni-tuebingen.de>
To: coq-club AT inria.fr
Subject: [Coq-Club] "Cannot satisfy constraint" error using subset types
Date: Sat, 29 Apr 2017 00:05:07 +0200
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.mailfrom=klaus.ostermann AT uni-tuebingen.de; spf=None smtp.helo=postmaster AT mx04.uni-tuebingen.de
Ironport-phdr: 9a23:L0qrgRbj5iE7b3aF8VSG0MH/LSx+4OfEezUN459isYplN5qZoMu+bnLW6fgltlLVR4KTs6sC0LuK9fi4EUU7or+5+EgYd5JNUxJXwe43pCcHRPC/NEvgMfTxZDY7FskRHHVs/nW8LFQHUJ2mPw6arXK99yMdFQviPgRpOOv1BpTSj8Oq3Oyu5pHfeQtFiT6ybL9oMBm6sRjau9ULj4dlNqs/0AbCrGFSe+RRy2NoJFaTkAj568yt4pNt8Dletuw4+cJYXqr0Y6o3TbpDDDQ7KG81/9HktQPCTQSU+HQRVHgdnwdSDAjE6BH6WYrxsjf/u+Fg1iSWIdH6QLYpUjmk8qxlSgLniD0fOjAn8G/Zl89+gqxVrx2uuxNxzJXZYJ2MNPdkYq/RYd0XSGhHU81MVyJBGIS8b44XAuQEOeZXtZT9p0ATphWnHgmsGP3gyiVNhnDs26061fkqHAbF3AwkBd0OrW/UoM/yNKcJTeC60rPIzTDZYPNQ3zfw85XIchYgof2VQbJwbNTexlIuFwPDgVWft4rlMymI2esTqmWW6fdrW+G3i2M/tg18rDeiyt0yhoXTho8Z0E7I+Th2zYotK9C1SlR3bcC4HJdNrS2XNZF6T8ciTmxupS000KcJuYShcygP0JknxwDQa/iAc4WQ5xLiW/qdLDhiiHJ4frK/hg++8VS9yuLiTca00VBKriVbndnKrHwCygLc5tCGSvt74EihxS6C2x3d5+xLO0w4i7DXJp47zrIui5YevlzPHirsl0X3iK+WeF8k+u+t6+n/YbXmooWTN5Jvig3kNaQugdC/DvoiMggLRWeb/+K82ab+/U3/QbVGl+E2krTHv5/BJMQboKG5DBFT0oo59hmwES+q0M4EknkfMFJFZBWHgpD1NFHJOfD0FOuwg1CxkDhw3P3GJb3gApDVLnfZirvhfLB961RdyAUp19xf6YhUWfk9J6f4XVa0v9jFBDc4NRa1yqDpEoZTzIQbDEGLC7KCeITJrVKS4+spJaHYZ4scpS27LOM56uTrhHk/sUIbfOy1wJYdaXa3E/IgL0jPMimkucsIDWpf5ll2d+ftklDXCTM=

I'm stuck at a strange error message where I can't find anything about
on this mailing list or the documentation.

It looks something like this:

Error:
In environment
...
fds : id -> id -> {n : nat & eqn n}
...
x1 : projT1 (fds f c) = length tys1
x2 : projT2 (fds f c) = {| e_xtor := c; e_xtor_tyargs := cv; e_body :=
term |}
The term "fds" has type "id -> id -> {n : nat & eqn n}"
while it is expected to have type "id -> id -> {n : nat & eqn n}" (cannot
satisfy constraint
"eqn (length tys1)" == "(fun n : nat => eqn n) (projT1 (fds f c))").

The types that it wants to be identical are identical, and they are also
identical
if all implicit arguments, universe levels etc. are printed. "eqn" is a
dependent
type that expects a "nat".

The constraint it cannot satisfy follows from equation x1, but Coq doesn't
seem to be able to use that assumption.

I'm rather clueless what to do about this error. Any suggestions?

Klaus

[Coq-Club] "Cannot satisfy constraint" error using subset types, Klaus Ostermann, 04/29/2017
- Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Jan Bessai, 04/29/2017
  - Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Klaus Ostermann, 04/29/2017
    - Re: [Coq-Club] "Cannot satisfy constraint" error using subset types, Jan Bessai, 04/30/2017