{-# OPTIONS --universe-polymorphism #-}
module T1 where

open import Data.Bool
open import Data.Unit
open import Data.Fin hiding ( _+_ ) renaming ( zero to fzero ; suc to fsuc ) 
open import Data.Nat
open import Data.Nat.Properties
open import Data.Product
open import Relation.Binary.PropositionalEquality
open ≡-Reasoning
import Algebra.RingSolver
open SemiringSolver

cP : ℕ → Polynomial 2
cP n = con n

data Norm : {p : Polynomial 2} → Normal 2 p → Set where
 ConstrNorm : {p : Polynomial 2} → Norm (normalise p)

normType : (p : Polynomial 2) → Set
normType p = Norm (normalise p)

normExp : (p : Polynomial 2) → Norm (normalise p)
normExp p = ConstrNorm

foo : Polynomial 2 → Polynomial 2
foo m = m :+ con 1

works : (m  : Polynomial 2) → normType (foo m)
works m = normExp (m :+ (cP 1))

fails : (m  : Polynomial 2) → normType (foo m)
fails m = normExp ((cP 1) :+ m)