coq-club AT inria.fr

Subject: The Coq mailing list

List archive

From: Vadim Zaliva <vzaliva AT cmu.edu>
To: coq-club AT inria.fr
Subject: [Coq-Club] incorrect type resolution
Date: Thu, 10 Nov 2016 17:41:01 -0800
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=vadim.zaliva AT west.cmu.edu; spf=Pass smtp.mailfrom=vadim.zaliva AT west.cmu.edu; spf=None smtp.helo=postmaster AT mail-wm0-f48.google.com
Ironport-phdr: 9a23:ZMvtGR/izVKBx/9uRHKM819IXTAuvvDOBiVQ1KB52+0cTK2v8tzYMVDF4r011RmSDN6ds68P0LCempujcFRI2YyGvnEGfc4EfD4+ouJSoTYdBtWYA1bwNv/gYn9yNs1DUFh44yPzahANS47xaFLIv3K98yMZFAnhOgppPOT1HZPZg9iq2+yo9ZDeZwtFiCChbb5yIxm7oxvdvdQKjIV/Lao81gHHqWZSdeRMwmNoK1OTnxLi6cq14ZVu7Sdete8/+sBZSan1cLg2QrJeDDQ9LmA6/9brugXZTQuO/XQTTGMbmQdVDgff7RH6WpDxsjbmtud4xSKXM9H6QawyVD+/6apgVR3mhzodNzMh8G/ZhM9+gr9Frh29vBFw2ZLYbZuPOfZiYq/Qf9UXTndBUMZLUCxBB5uxYIQVAOUcPOZYqpT2qFgUohu6BAmsGvngwSJPi3/o3Kw1yeAhEQDY3AM6BN8BrHHUrMjvOKgMTO+10bDFwDPeZP1VwTfw8IrFfx87rf2RQ759cdDdxEoxGw/fgVidqoroNC6P2OsXqWiU9e9gWPqvi2E5rwFxpSCixsI2hYnIgoIZ017F9SBlzIosK921R012bcSrEJtXsCGaOI92Td04T250vyY6z6UKuZ+9fCcU1JQq3xzSZvOdf4SV/B7uVPydLDRmiH5/d7+yhA6+8U26xe39Usm03kxKri1AktTUqHACzQHc6smCSvdn/0auwzKP1wHN6u5eOk01m7TUK4U9wrIqipUTtFnDEjXol0rrka+abl8k9fSw6+T7frXmoYeROJNzigHnK6ghhsi/AfkjPQUVRGia+eG81KX58kHjQbVKiOc2kqjDv5zAK8QbvP3xPwgA2YE6rh27Ej2O0dICnHBBIkgWVgiAit3XMl3PJbjKBPO+nV3kxCl5zvTHILTJCZDQaHXPjeGyLv5G90dAxV9rnphk7JVOB+RZLQ==

I am observing a strange problem which I could not easily replicate as a small example. I have a definition Foo with implicit parameter

Definition Foo {Ps: vector Rtheta 1 → Prop} (x:nat) := x.

When I try to reference it as

Definition bar {Ps} (x:nat) :=

@Foo Ps x.

the type of Ps is guessed incorrectly:

The term "Ps" has type "vector Rtheta 1 → Type"

while it is expected to have type "vector Rtheta 1 → Prop"

Any ideas what could be causing this? Declaring Ps' type explicitly helps:

Definition bar {Ps: vector Rtheta 1 -> Prop} (x:nat) :=

@Foo Ps x.

Using Coq 8.5pl3.

CMU ECE PhD candidate

Mobile: +1(510)220-1060