search

UlfNorell / agda-test

Agda test
0 stars 0 forks source link

Instance search for irrelevant/unused metas is started in wrong context #922

Closed UlfNorell closed 10 years ago

UlfNorell commented 10 years ago

From sattler....@gmail.com on October 21, 2013 17:26:01

The current development version reports the following error on the below program.

An internal error has occurred. Please report this as a bug. Location of the error: src/full/Agda/TypeChecking/Substitute.hs:322

module BugNo4 where

f : Set → Set → Set f x _ = x

module ( : f ? ?) where g = f

Original issue: http://code.google.com/p/agda/issues/detail?id=922

UlfNorell commented 10 years ago

From andreas....@gmail.com on October 21, 2013 13:31:09

Ah, Agda tries to solve the 2nd ? by instance search, since it is unused by f. I guess I did not fully understand the preconditions of calling the instance search, so it was started in the wrong context, leading to a piApply where there was no Pi, hence, to the crash.

Fix pushed.

Summary: Instance search for irrelevant/unused metas is started in wrong context (was: internal error (Substitute.hs:322) on minimal program)
Status: Fixed
Owner: andreas....@gmail.com
Labels: Type-Defect Instance Irrelevance