Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
weird compile error with proof for length indexed vector
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE PolyKinds #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE TypeInType #-}
module VectStuff where
import Data.Constraint ((:-)(Sub), Dict(Dict))
import Data.Kind (Type)
import Data.Singletons.Decide (Decision(Disproved, Proved), Refuted, (:~:)(Refl), (%~))
import Data.Singletons.Prelude (PNum((-)), sing)
import Data.Singletons.TypeLits (SNat, Sing(SNat))
import GHC.TypeLits (CmpNat, KnownNat, Nat)
import Unsafe.Coerce (unsafeCoerce)
data Vect :: Nat -> Type -> Type where
VNil :: Vect 0 a
VCons :: forall n a. CmpNat n 0 ~ 'GT => a -> Vect (n - 1) a -> Vect n a
instance Show a => Show (Vect n a) where
show = show . toListVect
toListVect :: Vect n a -> [a]
toListVect VNil = []
toListVect (VCons a v) = a : toListVect v
axiom :: Dict a
axiom = unsafeCoerce (Dict :: Dict ())
nGT0CmpNatLaw :: (Refuted (n :~: 0)) -> Dict (CmpNat n 0 ~ 'GT)
nGT0CmpNatLaw _ = axiom
cmpNatGT0KnownNatLaw :: forall n. (CmpNat n 0 ~ 'GT) :- KnownNat (n - 1)
cmpNatGT0KnownNatLaw = Sub axiom
sNatMinus1 :: forall n. (CmpNat n 0 ~ 'GT) => SNat n -> SNat (n - 1)
sNatMinus1 SNat =
case cmpNatGT0KnownNatLaw @n of
Sub Dict -> SNat
nGT0Proof :: forall n. Refuted (n :~: 0) -> SNat n -> (SNat (n - 1), Dict (KnownNat (n - 1)))
nGT0Proof f snat =
case nGT0CmpNatLaw f of
Dict ->
case cmpNatGT0KnownNatLaw @n of
Sub d -> (sNatMinus1 snat, d)
snatMinus1NGT0Law :: forall n. SNat (n - 1) -> Dict (CmpNat n 0 ~ 'GT)
snatMinus1NGT0Law _ = axiom
replicateVec :: forall n a. SNat n -> a -> Vect n a
replicateVec snat a =
case snat %~ (sing @_ @0) of
Proved Refl -> VNil
Disproved f ->
case nGT0Proof f snat of
(snat', Dict) ->
case snatMinus1NGT0Law @n snat' of
Dict ->
VCons a $ replicateVec snat' a
vec0 :: Vect 0 Char
vec0 = VNil
vec1 :: Vect 1 Char
vec1 = VCons 'a' vec0
vec2 :: Vect 2 Char
vec2 = VCons 'b' vec1
thisisweird :: Int
thisisweird =
case replicateVec (sing @_ @2) "4" of
VCons _ (efe :: Vect 1 String) ->
case efe of
VCons _ (jaja :: Vect 0 String) ->
-- This case causes the following error:
-- *** Exception: temp/what8.hs:(90,11)-(91,23): Non-exhaustive patterns in case
case jaja of
VNil -> 100
-- But adding a case for VCons causes a compile error:
--
-- temp/what8.hs:95:13: error:
-- • Couldn't match type ‘'EQ’ with ‘'GT’
-- Inaccessible code in
-- a pattern with constructor:
-- VCons :: forall (n :: Nat) a.
-- (CmpNat n 0 ~ 'GT) =>
-- a -> Vect (n - 1) a -> Vect n a,
-- in a case alternative
-- • In the pattern: VCons _ _
-- In a case alternative: VCons _ _ -> 200
-- In the expression:
-- case jaja of
-- VNil -> 100
-- VCons _ _ -> 200
-- |
-- 95 | VCons _ _ -> 200
-- | ^^^^^^^^^
-- Failed, no modules loaded.
--
-- VCons _ _ -> 200
@cdepillabout
Copy link
Author

cdepillabout commented Apr 7, 2018

Running the thisisweird function causes Non-exhaustive patterns in case or a compile error for some reason.

@cdepillabout
Copy link
Author

cdepillabout commented Apr 8, 2018

This is apparently because cmpNatGT0KnownNatLaw is wrong: https://stackoverflow.com/a/49710029/3040129

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment