content: {-# LANGUAGE KindSignatures      #-}
  {-# LANGUAGE DataKinds           #-}
  {-# LANGUAGE OverloadedStrings   #-}
  {-# LANGUAGE RankNTypes          #-}
  {-# LANGUAGE ScopedTypeVariables #-}
  {-# LANGUAGE GADTs               #-}
  {-@ LIQUID "--totality"        @-}
  {-@ LIQUID "--stringtheory"    @-}
  
  module StringIndexing where
  
  
  import GHC.TypeLits
  import Data.String 
  
  import Data.Proxy 
  -- Structure that defines valid indeces of a type level target 
  -- symbol in a value level string
  
  data MI (tagret :: Symbol) s where 
    MI :: IsString s => s        -- input string
                     -> [Int]    -- valid indeces of target in input
                     -> MI target s
  
  {-@ MI :: input:s 
         -> [{i:Int |	 subString input i (stringLen target)  == target }]
         -> MI s @-}
  
  
  -- STEP 1:    Verification of valid structures
  -- CHALLENGE: String interepretations from SMT 
  
  -- THESE SHOULD BE SAFE 
  misafe1 :: MI "cat" String 
  misafe1 = MI "catdogcatsdots" []
  
  misafe2 :: MI "cat" String
  misafe2 = MI "catdogcatsdots" [0]
  
  misafe3 :: MI "cat" String
  misafe3 = MI "catdogcatsdots" [0, 6]
  
  misafe4 :: MI "cat" String
  misafe4 = MI "catdogcatsdots" [6, 0]
  
  misafe5 :: MI "cat" String
  misafe5 = MI "catdogcatsdots" [6]
  
  
  -- THIS SHOULD BE UNSAFE 
  miunsafe :: MI "dog" String
  miunsafe = MI "catdogcatsdots" [1]
  