小编den*_*mal的帖子

我使用单一包生成的非常简单的类型级自然.我现在正在尝试向他们添加Ord实例.

{-# LANGUAGE MultiParamTypeClasses, TemplateHaskell, KindSignatures, DataKinds, ScopedTypeVariables, GADTs, TypeFamilies, FlexibleInstances, TypeOperators, UndecidableInstances, InstanceSigs #-}

module Functions where

import Data.Singletons
import Data.Singletons.TH
import Data.Singletons.Prelude
import Data.Promotion.Prelude

singletons [d|
             data Nat = Z | S Nat
               deriving Eq

             instance Ord Nat where
               (<=)    Z     _  = True
               (<=) (S _)    Z  = False
               (<=) (S n) (S m) = n <= m
             |]

我一直在遇到一个错误.最新的一个是:

src/Functions.hs:10:1:
    Couldn't match kind ‘Nat’ with ‘*’
    When matching types
      n0 :: Nat
      t1 :: *
    Expected …

我有一个表达:

gcastWith p1 $
gcastWith p2 $
e

这没问题.现在我试图将其重写为:

((gcastWith p1) .
 (gcastWith p2)) $
e

它不起作用(不是类型检查).但是这有效:

((gcastWith p1) .
 (gcastWith p2)) -- note I removed the dollar
e

我失去了关于如何了一些东西明显$和.操作？