Several failure cases for comp for polyadic fns and type variables

Description

Description

comp doesn't work for several common uses

Literal sets can't be used, neither can the well-known identity function

This seems to be a general problem with polyadic Fns

Environment

None

Activity

Show:
Oskar Wickström
December 11, 2014, 5:03 AM

I believe I have some similar problem, but I'm not sure if it's related. I'm not that into type theory so forgive me for any weird explanations. Hope this might add some value to the discussion though.

For better readability see this gist: https://gist.github.com/owickstrom/5695e0591ef245305f27

Marc O'Morain
May 7, 2015, 4:19 PM

I've hit a similar issue:

This will type-check correctly:

whereas this fails:

Ambrose Bonnaire-Sergeant
July 21, 2015, 5:27 AM

At least one of these problems requires a complete overhaul of the constraint generation algorithm.

Ambrose Bonnaire-Sergeant
December 3, 2017, 10:27 PM

Huge job, no current work towards this.

Assignee

Ambrose Bonnaire-Sergeant

Reporter

Herwig Hochleitner

Labels

None

Approval

None

Patch

None

Components

Fix versions

Priority

Minor
Configure