New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

termination checking failure in copattern-style definition #3218

Open
rntz opened this Issue Sep 6, 2018 · 0 comments

Comments

Projects
None yet
3 participants
@rntz

rntz commented Sep 6, 2018

I've run into a strange case where, if I combine two functions which are each individually accepted by the termination checker into a record value defined with copatterns, the termination checker rejects it:

postulate
  A : Set
  _≤_ : A  A  Set
  _•_ : {a b c}  a ≤ b  b ≤ c  a ≤ c

-- In the real world, these types would have other constructors, but I've
-- minimized them for this example.
data Tree : Set where node : Tree  Tree
data _⊑_ : Tree → Tree → Set where trans : {a b c}  a ⊑ b  b ⊑ c  a ⊑ c

record Fun : Set where
  field ap : Tree  A
  field map : {T U}  T ⊑ U  ap T ≤ ap U
open Fun

-- Consider the following definitions.
get : Tree  A
get (node T) = get T

Get : Fun
ap Get = get
map Get (trans T≤U U≤V) = map Get T≤U • map Get U≤V

-- If I try to combine these into a single definition, termination checking
-- fails. Why? :(
NoGet : Fun
ap NoGet (node T) = ap NoGet T
map NoGet (trans T≤U U≤V) = map NoGet T≤U • map NoGet U≤V

@gallais gallais added this to the 2.6.0 milestone Sep 6, 2018

@jespercockx jespercockx modified the milestones: 2.6.0, 2.6.1 Nov 15, 2018

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment