Movatterモバイル変換

{-# LANGUAGE DeriveGeneric          #-}{-# LANGUAGE TypeOperators          #-}{-# LANGUAGE GADTs                  #-}{-# LANGUAGE FlexibleInstances      #-}{-# LANGUAGE StandaloneDeriving     #-}{-# LANGUAGE NoImplicitPrelude      #-}{-# LANGUAGE RankNTypes             #-}{-# LANGUAGE TypeFamilies           #-}{-# LANGUAGE UndecidableInstances   #-}{-# LANGUAGE ExplicitNamespaces     #-}{-# LANGUAGE MultiParamTypeClasses  #-}{-# LANGUAGE FunctionalDependencies #-}{-# LANGUAGE DataKinds              #-}{-# LANGUAGE PolyKinds              #-}{-# LANGUAGE Trustworthy            #-}------------------------------------------------------------------------------- |-- Module      :  Data.Type.Equality-- License     :  BSD-style (see the LICENSE file in the distribution)---- Maintainer  :  libraries@haskell.org-- Stability   :  experimental-- Portability :  not portable---- Definition of propositional equality @(:~:)@. Pattern-matching on a variable-- of type @(a :~: b)@ produces a proof that @a ~ b@.---- @since 4.7.0.0-----------------------------------------------------------------------------moduleData.Type.Equality(-- * The equality types(:~:)(..),type(~~),(:~~:)(..),-- * Working with equalitysym,trans,castWith,gcastWith,apply,inner,outer,-- * Inferring equality from other typesTestEquality(..),-- * Boolean type-level equalitytype(==))whereimportData.MaybeimportGHC.EnumimportGHC.ShowimportGHC.ReadimportGHC.BaseimportData.Type.Bool-- | Lifted, homogeneous equality. By lifted, we mean that it can be-- bogus (deferred type error). By homogeneous, the two types @a@-- and @b@ must have the same kind.classa~~b=>(a::k)~(b::k)-- See Note [The equality types story] in TysPrim-- NB: All this class does is to wrap its superclass, which is--     the "real", inhomogeneous equality; this is needed when--     we have a Given (a~b), and we want to prove things from it-- NB: Not exported, as (~) is magical syntax. That's also why there's-- no fixity.-- It's tempting to put functional dependencies on (~), but it's not-- necessary because the functional-dependency coverage check looks-- through superclasses, and (~#) is handled in that check.-- | @since 4.9.0.0instance{-# INCOHERENT#-}a~~b=>a~b-- See Note [The equality types story] in TysPrim-- If we have a Wanted (t1 ~ t2), we want to immediately-- simplify it to (t1 ~~ t2) and solve that instead---- INCOHERENT because we want to use this instance eagerly, even when-- the tyvars are partially unknown.infix4:~:,:~~:-- | Propositional equality. If @a :~: b@ is inhabited by some terminating-- value, then the type @a@ is the same as the type @b@. To use this equality-- in practice, pattern-match on the @a :~: b@ to get out the @Refl@ constructor;-- in the body of the pattern-match, the compiler knows that @a ~ b@.---- @since 4.7.0.0dataa:~:bwhere-- See Note [The equality types story] in TysPrimRefl::a:~:a-- with credit to Conal Elliott for 'ty', Erik Hesselink & Martijn van-- Steenbergen for 'type-equality', Edward Kmett for 'eq', and Gabor Greif-- for 'type-eq'-- | Symmetry of equalitysym::(a:~:b)->(b:~:a)symRefl=Refl-- | Transitivity of equalitytrans::(a:~:b)->(b:~:c)->(a:~:c)transReflRefl=Refl-- | Type-safe cast, using propositional equalitycastWith::(a:~:b)->a->bcastWithReflx=x-- | Generalized form of type-safe cast using propositional equalitygcastWith::(a:~:b)->((a~b)=>r)->rgcastWithReflx=x-- | Apply one equality to another, respectivelyapply::(f:~:g)->(a:~:b)->(fa:~:gb)applyReflRefl=Refl-- | Extract equality of the arguments from an equality of applied typesinner::(fa:~:gb)->(a:~:b)innerRefl=Refl-- | Extract equality of type constructors from an equality of applied typesouter::(fa:~:gb)->(f:~:g)outerRefl=Refl-- | @since 4.7.0.0derivinginstanceEq(a:~:b)-- | @since 4.7.0.0derivinginstanceShow(a:~:b)-- | @since 4.7.0.0derivinginstanceOrd(a:~:b)-- | @since 4.7.0.0derivinginstancea~b=>Read(a:~:b)-- | @since 4.7.0.0instancea~b=>Enum(a:~:b)wheretoEnum0=RefltoEnum_=errorWithoutStackTrace"Data.Type.Equality.toEnum: bad argument"fromEnumRefl=0-- | @since 4.7.0.0derivinginstancea~b=>Bounded(a:~:b)-- | Kind heterogeneous propositional equality. Like ':~:', @a :~~: b@ is-- inhabited by a terminating value if and only if @a@ is the same type as @b@.---- @since 4.10.0.0data(a::k1):~~:(b::k2)whereHRefl::a:~~:a-- | @since 4.10.0.0derivinginstanceEq(a:~~:b)-- | @since 4.10.0.0derivinginstanceShow(a:~~:b)-- | @since 4.10.0.0derivinginstanceOrd(a:~~:b)-- | @since 4.10.0.0derivinginstancea~~b=>Read(a:~~:b)-- | @since 4.10.0.0instancea~~b=>Enum(a:~~:b)wheretoEnum0=HRefltoEnum_=errorWithoutStackTrace"Data.Type.Equality.toEnum: bad argument"fromEnumHRefl=0-- | @since 4.10.0.0derivinginstancea~~b=>Bounded(a:~~:b)-- | This class contains types where you can learn the equality of two types-- from information contained in /terms/. Typically, only singleton types should-- inhabit this class.classTestEqualityfwhere-- | Conditionally prove the equality of @a@ and @b@.testEquality::fa->fb->Maybe(a:~:b)-- | @since 4.7.0.0instanceTestEquality((:~:)a)wheretestEqualityReflRefl=JustRefl-- | @since 4.10.0.0instanceTestEquality((:~~:)a)wheretestEqualityHReflHRefl=JustReflinfix4==-- | A type family to compute Boolean equality.typefamily(a::k)==(b::k)::Boolwherefa==gb=f==g&&a==ba==a='True_==_='False-- The idea here is to recognize equality of *applications* using-- the first case, and of *constructors* using the second and third-- ones. It would be wonderful if GHC recognized that the-- first and second cases are compatible, which would allow us to-- prove---- a ~ b => a == b---- but it (understandably) does not.---- It is absolutely critical that the three cases occur in precisely-- this order. In particular, if---- a == a = 'True---- came first, then the type application case would only be reached-- (uselessly) when GHC discovered that the types were not equal.---- One might reasonably ask what's wrong with a simpler version:---- type family (a :: k) == (b :: k) where--  a == a = True--  a == b = False---- Consider-- data Nat = Zero | Succ Nat---- Suppose I want-- foo :: (Succ n == Succ m) ~ True => ((n == m) :~: True)-- foo = Refl---- This would not type-check with the simple version. `Succ n == Succ m`-- is stuck. We don't know enough about `n` and `m` to reduce the family.-- With the recursive version, `Succ n == Succ m` reduces to-- `Succ == Succ && n == m`, which can reduce to `'True && n == m` and-- finally to `n == m`.