--type-based-termination does not process postulates

[andreasabel]

The mapRose example passes with defined List and mapList but fails when we turn them into postulates:

{-# OPTIONS --type-based-termination #-}
{-# OPTIONS --no-syntax-based-termination #-}

{-# OPTIONS -v term.tbt:50 #-}

variable
  A B : Set

module PostulatedList where

  {-# POLARITY List ++ #-}

  postulate
    List : Set → Set
    mapList : (A → B) → List A → List B

module DefinedList where

  data List A : Set where
    [] : List A
    _∷_ : A → List A → List A

  mapList : (A → B) → List A → List B
  mapList f [] = []
  mapList f (x ∷ xs) = f x ∷ mapList f xs

open PostulatedList  -- type-based termination complains
-- open DefinedList -- type-based termination succeeds

data Rose (A : Set) : Set where
  rose : List (Rose A) → Rose A

mapRose : (A → B) → Rose A → Rose B
mapRose f (rose rs) = rose (mapList (mapRose f) rs)

It should not matter how mapList is defined as long as it is parametric. ATTN: @knisht

[knisht]

Ok, I guess we don't need to protect type-based termination from postulates. The mere presence of them indicates that we are out of the safe zone.

[knisht]

This particular example exposes another problem: I do not support polarities yet. Maybe it makes sense to delay it until #6385 is merged.

[andreasabel]

Postulates should be handled like things in the context, e.g. module parameters. The following is (correctly) accepted:

{-# OPTIONS --type-based-termination #-}

data List A : Set where
  [] : List A
  _∷_ : A → List A → List A

module _ (mapList : {A B : Set} → (A → B) → List A → List B) where

  data Rose (A : Set) : Set where
    rose : List (Rose A) → Rose A

  mapRose : {A B : Set} → (A → B) → Rose A → Rose B
  mapRose f (rose rs) = rose (mapList (mapRose f) rs)