    {-# LANGUAGE CPP, PatternGuards #-}

    module Agda.TypeChecking.Conversion where

    import Control.Applicative
    import Control.Monad
    import Control.Monad.State
    import Control.Monad.Error
    import Data.Generics
    import Data.Traversable hiding (mapM, sequence)
    import Data.List hiding (sort)
    import qualified Data.List as List

    import Agda.Syntax.Literal
    import Agda.Syntax.Common
    import Agda.Syntax.Internal
    import Agda.TypeChecking.Monad
    import Agda.TypeChecking.MetaVars
    import Agda.TypeChecking.Substitute
    import Agda.TypeChecking.Reduce
    import Agda.TypeChecking.Constraints
    import Agda.TypeChecking.Errors
    import Agda.TypeChecking.Primitive (constructorForm)
    import Agda.TypeChecking.Free
    import Agda.TypeChecking.Records
    import Agda.TypeChecking.Pretty
    import Agda.TypeChecking.Injectivity
    import Agda.TypeChecking.SizedTypes
    import Agda.TypeChecking.Monad.Builtin
    import Agda.TypeChecking.Level

    import Agda.Utils.Monad

    import Agda.TypeChecking.Monad.Debug

    #include "../undefined.h"
    import Agda.Utils.Impossible

    nextPolarity []       = (Invariant, [])
    nextPolarity (p : ps) = (p, ps)

    -- | Check if to lists of arguments are the same (and all variables).
    --   Precondition: the lists have the same length.
    sameVars :: Args -> Args -> Bool
    sameVars xs ys = and $ zipWith same xs ys
        where
    	same (Arg _ (Var n [])) (Arg _ (Var m [])) = n == m
    	same _ _				   = False

    equalTerm :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
    equalTerm = compareTerm CmpEq

    equalAtom :: MonadTCM tcm => Type -> Term -> Term -> tcm Constraints
    equalAtom = compareAtom CmpEq

    equalArgs :: MonadTCM tcm => Type -> Args -> Args -> tcm Constraints
    equalArgs = compareArgs []

    equalType :: MonadTCM tcm => Type -> Type -> tcm Constraints
    equalType = compareType CmpEq

    -- | Type directed equality on values.
    --
    compareTerm :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
    compareTerm cmp a m n =
      catchConstraint (ValueCmp cmp a m n) $ do
        a'       <- reduce a
        reportSDoc "tc.conv.term" 10 $ fsep
          [ text "compareTerm", prettyTCM m, prettyTCM cmp, prettyTCM n, text ":", prettyTCM a' ]
        proofIrr <- proofIrrelevance
        isSize   <- isSizeType a'
        s        <- reduce $ getSort a'
        mlvl     <- liftTCM $ (Just <$> primLevel) `catchError` \_ -> return Nothing
        case s of
          Prop | proofIrr -> return []
          _    | isSize   -> compareSizes cmp m n
          _               -> case unEl a' of
            a | Just a == mlvl && cmp == CmpEq -> equalLevel m n
            Pi a _    -> equalFun (a,a') m n
            Fun a _   -> equalFun (a,a') m n
            MetaV x _ -> do
              (m,n) <- normalise (m,n)
              if m == n
                then return []
                else buildConstraint (ValueCmp cmp a m n)
            Lam _ _   -> __IMPOSSIBLE__
            Def r ps  -> do
              isrec <- isRecord r
              if isrec
                then do
                  m <- reduceB m
                  n <- reduceB n
                  case (m, n) of
                    _ | isNeutral m && isNeutral n ->
                        compareAtom cmp a' (ignoreBlocking m) (ignoreBlocking n)
                    _ -> do
                      (tel, m') <- etaExpandRecord r ps $ ignoreBlocking m
                      (_  , n') <- etaExpandRecord r ps $ ignoreBlocking n
                      -- No subtyping on record terms
                      compareArgs [] (telePi_ tel $ sort Prop) m' n'
                else compareAtom cmp a' m n
            _ -> compareAtom cmp a' m n
      where
        isNeutral Blocked{}          = False
        isNeutral (NotBlocked Con{}) = False
        isNeutral _                  = True

        equalFun (a,t) m n = do
            name <- freshName_ (suggest $ unEl t)
            addCtx name a $ compareTerm cmp t' m' n'
          where
            p	= fmap (const $ Var 0 []) a
            (m',n') = raise 1 (m,n) `apply` [p]
            t'	= raise 1 t `piApply` [p]
            suggest (Fun _ _)	 = "x"
            suggest (Pi _ (Abs x _)) = x
            suggest _		 = __IMPOSSIBLE__

    compareTel :: MonadTCM tcm => Comparison -> Telescope -> Telescope -> tcm Constraints
    compareTel cmp tel1 tel2 =
      catchConstraint (TelCmp cmp tel1 tel2) $ case (tel1, tel2) of
        (EmptyTel, EmptyTel) -> return []
        (EmptyTel, _)        -> bad
        (_, EmptyTel)        -> bad
        (ExtendTel arg1@(Arg h1 a1) tel1, ExtendTel arg2@(Arg h2 a2) tel2)
          | h1 /= h2  -> bad
          | otherwise -> do
              let (tel1', tel2') = raise 1 (tel1, tel2)
                  arg            = Var 0 []
              name <- freshName_ (suggest (absName tel1) (absName tel2))
              cs   <- compareType cmp a1 a2
              let c = TelCmp cmp (absApp tel1' arg) (absApp tel2' arg)

    	  let dependent = 0 `freeIn` absBody tel2

              if dependent
    	    then addCtx name arg1 $ guardConstraint (return cs) c
    	    else do cs' <- addCtx name arg1 $ solveConstraint c
    		    return $ cs ++ cs'
              where
                suggest "_" y = y
                suggest  x  _ = x
      where
        bad = typeError $ UnequalTelescopes cmp tel1 tel2

    -- | Syntax directed equality on atomic values
    --
    compareAtom :: MonadTCM tcm => Comparison -> Type -> Term -> Term -> tcm Constraints
    compareAtom cmp t m n =
        catchConstraint (ValueCmp cmp t m n) $ do
          mb <- traverse constructorForm =<< reduceB m
          nb <- traverse constructorForm =<< reduceB n
          let m = ignoreBlocking mb
              n = ignoreBlocking nb
          reportSDoc "tc.conv.atom" 10 $ fsep
    	[ text "compareAtom", prettyTCM mb, prettyTCM cmp, prettyTCM nb, text ":", prettyTCM t ]
          case (mb, nb) of
            (NotBlocked (MetaV x xArgs), NotBlocked (MetaV y yArgs))
                | x == y -> if   sameVars xArgs yArgs
                            then return []
                            else do -- Check syntactic equality on meta-variables
                                    -- (same as for blocked terms)
                              m <- normalise m
                              n <- normalise n
                              if m == n
                                then return []
                                else buildConstraint (ValueCmp cmp t m n)
                | otherwise -> do
                    [p1, p2] <- mapM getMetaPriority [x,y]
                    -- instantiate later meta variables first
                    let (solve1, solve2)
                          | (p1,x) > (p2,y) = (l,r)
                          | otherwise	    = (r,l)
                          where l = assignV t x xArgs n
                                r = assignV t y yArgs m
                        try m fallback = do
                          cs <- m
                          case cs of
                            []	-> return []
                            _	-> fallback cs

                    -- First try the one with the highest priority. If that doesn't
                    -- work, try the low priority one. If that doesn't work either,
                    -- go with the first version.
                    rollback <- return . put =<< get
                    try solve1 $ \cs -> do
                      undoRollback <- return . put =<< get
                      rollback
                      try solve2 $ \_ -> do
                        undoRollback
                        return cs

    	(NotBlocked (MetaV x xArgs), _) -> assignV t x xArgs n
    	(_, NotBlocked (MetaV x xArgs)) -> assignV t x xArgs m
            (Blocked{}, Blocked{})	-> do
                n <- normalise n    -- is this what we want?
                m <- normalise m
                if m == n
                    then return []	-- Check syntactic equality for blocked terms
                    else buildConstraint $ ValueCmp cmp t m n
            (Blocked{}, _)    -> useInjectivity cmp t m n
            (_,Blocked{})     -> useInjectivity cmp t m n
            _ -> case (m, n) of
    	    _ | f1@(FunV _ _) <- funView m
    	      , f2@(FunV _ _) <- funView n -> equalFun f1 f2

    	    (Sort s1, Sort s2) -> compareSort CmpEq s1 s2

    	    (Lit l1, Lit l2) | l1 == l2 -> return []
    	    (Var i iArgs, Var j jArgs) | i == j -> do
    		a <- typeOfBV i
                    -- Variables are invariant in their arguments
    		compareArgs [] a iArgs jArgs
    	    (Def x xArgs, Def y yArgs) | x == y -> do
                    pol <- getPolarity' cmp x
    		reportSDoc "tc.conv.atom" 20 $
    		  text "compareArgs" <+> sep
                        [ sep [ prettyTCM xArgs
    			  , prettyTCM yArgs
    			  ]
                        , nest 2 $ text (show pol)
                        ]
    		a <- defType <$> getConstInfo x
    		compareArgs pol a xArgs yArgs
    	    (Con x xArgs, Con y yArgs)
    		| x == y -> do
    		    -- The type is a datatype.
    		    Def d args <- reduce $ unEl t
    		    -- Get the number of parameters to the datatype
    		    Datatype{dataPars = npars} <- theDef <$> getConstInfo d
    		    -- The type to compare the arguments at is obtained by
    		    -- instantiating the parameters.
    		    a <- defType <$> getConstInfo x
    		    let a' = piApply a (genericTake npars args)
                        -- Constructors are invariant in their arguments
                        -- (could be covariant).
                        compareArgs [] a' xArgs yArgs
                _ -> typeError $ UnequalTerms cmp m n t
        where
    	equalFun (FunV arg1@(Arg h1 a1) t1) (FunV (Arg h2 a2) t2)
    	    | h1 /= h2	= typeError $ UnequalHiding ty1 ty2
    	    | otherwise = do
    		    let (ty1',ty2') = raise 1 (ty1,ty2)
    			arg	    = Arg h1 (Var 0 [])
    		    name <- freshName_ (suggest t1 t2)
    		    cs   <- compareType cmp a2 a1
    		    let c = TypeCmp cmp (piApply ty1' [arg]) (piApply ty2' [arg])

    		    -- We only need to require a1 == a2 if t2 is a dependent function type.
    		    -- If it's non-dependent it doesn't matter what we add to the context.
    		    let dependent = case t2 of
    					Pi _ _	-> True
    					Fun _ _	-> False
    					_	-> __IMPOSSIBLE__
    		    if dependent
    			then addCtx name arg1 $ guardConstraint (return cs) c
    			else do
    			    cs' <- addCtx name arg1 $ solveConstraint c
    			    return $ cs ++ cs'
    	    where
    		ty1 = El (getSort a1) t1    -- TODO: wrong (but it doesn't matter)
    		ty2 = El (getSort a2) t2
    		suggest t1 t2 = case concatMap name [t1,t2] of
    				    []	-> "_"
    				    x:_	-> x
    		    where
    			name (Pi _ (Abs x _)) = [x]
    			name (Fun _ _)	      = []
    			name _		      = __IMPOSSIBLE__
    	equalFun _ _ = __IMPOSSIBLE__

    -- | Type-directed equality on argument lists
    --
    compareArgs :: MonadTCM tcm => [Polarity] -> Type -> Args -> Args -> tcm Constraints
    compareArgs _ _ [] [] = return []
    compareArgs _ _ [] (_:_) = __IMPOSSIBLE__
    compareArgs _ _ (_:_) [] = __IMPOSSIBLE__
    compareArgs pols0 a (arg1 : args1) (arg2 : args2) = do
        let (pol, pols) = nextPolarity pols0
        a <- reduce a
        reportSDoc "tc.conv.args" 30 $
          sep [ text "compareArgs"
              , nest 2 $ sep [ prettyTCM (arg1 : args1)
                             , prettyTCM (arg2 : args2)
                             ]
              , nest 2 $ text ":" <+> prettyTCM a
              ]
        case funView (unEl a) of
    	FunV (Arg _ b) _ -> do
    	    reportSDoc "tc.conv.args" 10 $
                  sep [ text "compareArgs" <+> parens (text $ show pol)
                      , nest 2 $ sep [ prettyTCM arg1
                                     , text "~~" <+> prettyTCM arg2
                                     , text ":" <+> prettyTCM b
                                     ]
                      ]
                let cmp x y = case pol of
                                Invariant     -> compareTerm CmpEq b x y
                                Covariant     -> compareTerm CmpLeq b x y
                                Contravariant -> compareTerm CmpLeq b y x
                cs1 <- cmp (unArg arg1) (unArg arg2)
    	    case (cs1, unEl a) of
                                    -- We can safely ignore sort annotations here.
    		(_:_, Pi _ c) | 0 `freeInIgnoringSorts` absBody c
    		    -> do
                            reportSDoc "tc.conv.args" 15 $ sep
                              [ text "aborting compareArgs" <+> parens (text $ show pol)
                              , nest 2 $ fsep
                                  [ prettyTCM arg1
                                  , text "~~" <+> prettyTCM arg2
                                  , text ":" <+> prettyTCM b
                                  , text "--->" <+> prettyTCM cs1
                                  ]
                              ]
                            patternViolation   -- TODO: will duplicate work (all arguments checked so far)
    		_   -> do
                        reportSDoc "tc.conv.args" 15 $ sep
                          [ text "compareArgs" <+> parens (text $ show pol)
                          , nest 2 $ sep
                            [ prettyTCM arg1
                            , text "~~" <+> prettyTCM arg2
                            , text ":" <+> prettyTCM (piApply a [arg1])
                            ]
                          ]
    		    cs2 <- compareArgs pols (piApply a [arg1]) args1 args2
    		    return $ cs1 ++ cs2
            _   -> patternViolation

    -- | Equality on Types
    compareType :: MonadTCM tcm => Comparison -> Type -> Type -> tcm Constraints
    compareType cmp ty1@(El s1 a1) ty2@(El s2 a2) =
        catchConstraint (TypeCmp cmp ty1 ty2) $ do
    	reportSDoc "tc.conv.type" 9 $ vcat
              [ hsep [ text "compareType", prettyTCM ty1, prettyTCM cmp, prettyTCM ty2 ]
              , hsep [ text "   sorts:", prettyTCM s1, text " and ", prettyTCM s2 ]
              ]
    	cs1 <- compareSort CmpEq s1 s2 `catchError` \err -> case errError err of
                      TypeError _ _ -> do
                        -- This error will probably be more informative
                        compareTerm cmp (sort s1) a1 a2
                        -- Throw the original error if the above doesn't
                        -- give an error (for instance, due to pending
                        -- constraints).
                        throwError err
                      _             -> throwError err
    	cs2 <- compareTerm cmp (sort s1) a1 a2
            cs  <- solveConstraints $ cs1 ++ cs2
            unless (null cs) $
              reportSDoc "tc.conv.type" 9 $
                text "   --> " <+> prettyTCM cs
    	return cs

    leqType :: MonadTCM tcm => Type -> Type -> tcm Constraints
    leqType = compareType CmpLeq

    ---------------------------------------------------------------------------
    -- * Sorts
    ---------------------------------------------------------------------------

    compareSort :: MonadTCM tcm => Comparison -> Sort -> Sort -> tcm Constraints
    compareSort CmpEq  = equalSort
    compareSort CmpLeq = leqSort
      -- TODO: change to leqSort when we have better constraint solving
      --       or not? might not be needed if we get universe polymorphism
      --       leqSort is still used when checking datatype declarations though

    -- | Check that the first sort is less or equal to the second.
    leqSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
    leqSort s1 s2 =
      ifM typeInType (return []) $
        catchConstraint (SortCmp CmpLeq s1 s2) $
        do	(s1,s2) <- reduce (s1,s2)
            reportSDoc "tc.conv.sort" 10 $
              sep [ text "leqSort"
                  , nest 2 $ fsep [ prettyTCM s1 <+> text "=<"
                                  , prettyTCM s2 ]
                  ]
    	case (s1,s2) of

    	    (Prop    , Prop    )	     -> return []
    	    (Type _  , Prop    )	     -> notLeq s1 s2
    	    (Suc _   , Prop    )	     -> notLeq s1 s2

    	    (Prop    , Type _  )	     -> return []
    	    (Type (Lit (LitLevel _ n)), Type (Lit (LitLevel _ m)))
                  | n <= m    -> return []
    	      | otherwise -> notLeq s1 s2
                (Type a, Type b) -> leqLevel a b

    	    (Suc s   , Type (Lit (LitLevel _ n)))
                  | 1 <= n    -> leqSort s (mkType $ n - 1)
    	    (Suc s   , Type b  ) -> notLeq s1 s2  -- TODO
                (Suc s1  , Suc s2  ) -> leqSort s1 s2 -- TODO: not what we want for Prop(?)
    	    (_	     , Suc _   )	     -> equalSort s1 s2

    	    (Lub a b , _       )	     -> liftM2 (++) (leqSort a s2) (leqSort b s2)
    	    (_	     , Lub _ _ )	     -> equalSort s1 s2

    	    (MetaS{} , _       )	     -> equalSort s1 s2
    	    (_	     , MetaS{} )	     -> equalSort s1 s2
                (Inf     , Inf     )             -> return []
                (Inf     , _       )             -> notLeq s1 s2
                (_       , Inf     )             -> return []
                (DLub{}  , _       )             -> equalSort s1 s2
                (_       , DLub{}  )             -> equalSort s1 s2
        where
    	notLeq s1 s2 = typeError $ NotLeqSort s1 s2

    leqLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
    leqLevel a b = liftTCM $ do
      reportSDoc "tc.conv.nat" 10 $
        text "compareLevel" <+>
          sep [ prettyTCM a <+> text "=<"
              , prettyTCM b ]
      n <- levelView a
      m <- levelView b
      leqView n m
      where
        leqView n@(Max as) m@(Max bs) = do
          reportSDoc "tc.conv.nat" 10 $
            text "compareLevelView" <+>
              sep [ text (show n) <+> text "=<"
                  , text (show m) ]
          case (as, bs) of
            (_, [])  -> concat <$> sequence [ leqPlusView a (ClosedLevel 0) | a <- as ]
            (_, [b]) -> concat <$> sequence [ leqPlusView a b | a <- as ]
            _        -> do
              -- Each a needs to be less than at least one of the b's
              sequence [ choice [ leqPlusView a b | b <- bs ] | a <- as ]
              return []
        leqPlusView n m = do
          reportSDoc "tc.conv.nat" 10 $
            text "comparePlusView" <+>
              sep [ text (show n) <+> text "=<"
                  , text (show m) ]
          case (n, m) of
            -- Both closed
            (ClosedLevel n, ClosedLevel m)
              | n <= m -> ok

            -- Both neutral
            (Plus n (NeutralLevel a), Plus m (NeutralLevel b))
              | n <= m -> do
                lvl <- primLevel
                equalTerm (El (mkType 0) lvl) a b

            -- closed ≤ any
            (ClosedLevel n, Plus m _)
              | n <= m -> ok

            -- Any blocked or meta
            (Plus _ BlockedLevel{}, _) -> postpone
            (_, Plus _ BlockedLevel{}) -> postpone
            (Plus _ MetaLevel{}, _)    -> postpone
            (_, Plus _ MetaLevel{})    -> postpone

            _ -> notok
        ok       = return []
        notok    = typeError $ NotLeqSort (Type a) (Type b)
        postpone = patternViolation

        choice []     = patternViolation
        choice (m:ms) = noConstraints m `catchError` \_ -> choice ms
    --       case errError e of
    --         PatternErr{} -> choice ms
    --         _            -> throwError e

    equalLevel :: MonadTCM tcm => Term -> Term -> tcm Constraints
    equalLevel a b = do
      Max as <- levelView a
      Max bs <- levelView b
      a <- unLevelView (Max as)
      b <- unLevelView (Max bs)
      liftTCM $ check a b as bs
      where
        check a b as bs = do
          let getLvl = El (mkType 0) <$> primLevel
          reportSDoc "tc.conv.nat" 20 $
            sep [ text "equalLevel"
                , nest 2 $ sep [ prettyTCM a <+> text "=="
                               , prettyTCM b
                               ]
                , nest 2 $ sep [ text (show (Max as)) <+> text "=="
                               , text (show (Max bs))
                               ]
                ]
          let a === b   = do
                lvl <- getLvl
                equalAtom lvl a b
              as =!= bs = do a <- unLevelView (Max as)
                             b <- unLevelView (Max bs)
                             a === b
          case (as, bs) of
            _ | List.sort as == List.sort bs -> ok
              | any isBlocked (as ++ bs) -> do
                  lvl <- getLvl
                  liftTCM $ useInjectivity CmpEq lvl a b

            -- 0 == any
            ([], _) -> wrap $ concat <$> sequence [ as =!= [b] | b <- bs ]
            (_, []) -> wrap $ concat <$> sequence [ [a] =!= bs | a <- as ]

            -- closed == closed
            ([ClosedLevel n], [ClosedLevel m])
              | n == m    -> ok
              | otherwise -> notok

            -- closed == neutral
            ([ClosedLevel{}], _) | any isNeutral bs -> notok
            (_, [ClosedLevel{}]) | any isNeutral as -> notok

            -- meta == any
            ([Plus n (MetaLevel x as)], _)
              | any (isThisMeta x) bs -> postpone
              | otherwise             -> do
                bs' <- mapM (subtr n) bs
                lvl <- getLvl
                assignV lvl x as =<< unLevelView (Max bs')
            (_, [Plus n (MetaLevel x bs)])
              | any (isThisMeta x) as -> postpone
              | otherwise             -> do
                as' <- mapM (subtr n) as
                lvl <- getLvl
                assignV lvl x bs =<< unLevelView (Max as')

            -- any other metas
            _ | any isMeta (as ++ bs) -> postpone

            -- neutral/closed == neutral/closed
            _ | all isNeutralOrClosed (as ++ bs) -> as =!= bs

            -- more cases?
            _ -> postpone

          where
            ok       = return []
            notok    = typeError $ UnequalSorts (Type a) (Type b)
            postpone = patternViolation

            -- Make sure to give a sensible error message
            wrap m = m `catchError` \err ->
              case errError err of
                TypeError{} -> notok
                _           -> throwError err

            subtr n (ClosedLevel m)
              | m >= n    = return $ ClosedLevel (m - n)
              | otherwise = notok
            subtr n (Plus m a)
              | m >= n    = return $ Plus (m - n) a
            subtr _ (Plus _ BlockedLevel{}) = postpone
            subtr _ (Plus _ MetaLevel{})    = postpone
            subtr _ (Plus _ NeutralLevel{}) = notok

            isNeutral (Plus _ NeutralLevel{}) = True
            isNeutral _                       = False

            isClosed ClosedLevel{} = True
            isClosed _             = False

            isNeutralOrClosed l = isClosed l || isNeutral l

            isBlocked (Plus _ BlockedLevel{}) = True
            isBlocked _                     = False

            isMeta (Plus _ MetaLevel{}) = True
            isMeta _                  = False

            isThisMeta x (Plus _ (MetaLevel y _)) = x == y
            isThisMeta _ _                      = False

    -- | Check that the first sort equal to the second.
    equalSort :: MonadTCM tcm => Sort -> Sort -> tcm Constraints
    equalSort s1 s2 =
      ifM typeInType (return []) $
        catchConstraint (SortCmp CmpEq s1 s2) $ do
            (s1,s2) <- reduce (s1,s2)
            reportSDoc "tc.conv.sort" 10 $
              sep [ text "equalSort"
                  , nest 2 $ fsep [ prettyTCM s1 <+> text "=="
                                  , prettyTCM s2 ]
                  ]
    	case (s1,s2) of

    	    (MetaS x us , MetaS y vs) -> do
                  s1 <- normalise s1
                  s2 <- normalise s2
                  if s1 == s2 then return []
    			  else do
    		[p1, p2] <- mapM getMetaPriority [x, y]
    		if p1 >= p2 then assignS x us s2
    			    else assignS y vs s1
    	    (MetaS x vs, _       ) -> assignS x vs s2
    	    (_	     , MetaS{} ) -> equalSort s2 s1

    	    (Prop    , Prop    ) -> return []
    	    (Type _  , Prop    ) -> notEq s1 s2
    	    (Prop    , Type _  ) -> notEq s1 s2

                (Type (Lit n), Type (Lit m))
                  | n == m           -> return []
                  | otherwise        -> notEq s1 s2
                (Type a  , Type b  ) -> equalLevel a b
    	    (Suc s   , Prop    ) -> notEq s1 s2
    	    (Suc s   , Type (Lit (LitLevel _ 0))) -> notEq s1 s2
    	    (Suc s   , Type (Lit (LitLevel _ 1))) -> buildConstraint (SortCmp CmpEq s1 s2)
    	    (Suc s   , Type (Lit (LitLevel _ n))) -> equalSort s (mkType $ n - 1)
    	    (Prop    , Suc s   ) -> notEq s1 s2
    	    (Type (Lit (LitLevel _ 0))  , Suc s   ) -> notEq s1 s2
    	    (Type (Lit (LitLevel _ 1))  , Suc s   ) -> buildConstraint (SortCmp CmpEq s1 s2)
    	    (Type (Lit (LitLevel _ n))  , Suc s   ) -> equalSort (mkType $ n - 1) s
                (Suc s1  , Suc s2  ) -> equalSort s1 s2 -- TODO: not what we want for Prop(?)
    	    (_	     , Suc _   ) -> buildConstraint (SortCmp CmpEq s1 s2)
    	    (Suc _   , _       ) -> buildConstraint (SortCmp CmpEq s1 s2)

                (Inf     , Inf     )             -> return []
                (Inf     , _       )             -> notEq s1 s2
                (_       , Inf     )             -> notEq s1 s2
                (s0@(Type (Lit (LitLevel _ 0))), Lub s1 s2) -> do
                  cs1 <- equalSort s0 s1
                  cs2 <- equalSort s0 s2
                  return $ cs1 ++ cs2
                (Lub s1 s2, s0@(Type (Lit (LitLevel _ 0)))) -> do
                  cs1 <- equalSort s1 s0
                  cs2 <- equalSort s2 s0
                  return $ cs1 ++ cs2
                (Lub{}   , Lub{}   ) -> do
                  (s1, s2) <- normalise (s1, s2)
                  if s1 == s2
                    then return []
                    else buildConstraint (SortCmp CmpEq s1 s2)
    	    (Lub _ _ , _       ) -> buildConstraint (SortCmp CmpEq s1 s2)
    	    (_	     , Lub _ _ ) -> buildConstraint (SortCmp CmpEq s1 s2)

                (DLub s1 s2, s0@(Type (Lit (LitLevel _ 0)))) -> do
                  cs1 <- equalSort s1 s0
                  cs2 <- underAbstraction_ s2 $ \s2 -> equalSort s2 s0
                  return $ cs1 ++ cs2
                (s0@(Type (Lit (LitLevel _ 0))), DLub s1 s2) -> do
                  cs1 <- equalSort s0 s1
                  cs2 <- underAbstraction_ s2 $ \s2 -> equalSort s0 s2
                  return $ cs1 ++ cs2
                (DLub{}  , _       )             -> buildConstraint (SortCmp CmpEq s1 s2)
                (_       , DLub{}  )             -> buildConstraint (SortCmp CmpEq s1 s2)
        where
    	notEq s1 s2 = typeError $ UnequalSorts s1 s2