diff --git a/LICENSE b/LICENSE
new file mode 100644
--- /dev/null
+++ b/LICENSE
@@ -0,0 +1,26 @@
+Copyright 2025 Author name here
+
+Redistribution and use in source and binary forms, with or without
+modification, are permitted provided that the following conditions are met:
+
+1.  Redistributions of source code must retain the above copyright notice, this
+    list of conditions and the following disclaimer.
+
+2.  Redistributions in binary form must reproduce the above copyright notice,
+    this list of conditions and the following disclaimer in the documentation
+    and/or other materials provided with the distribution.
+
+3.  Neither the name of the copyright holder nor the names of its contributors
+    may be used to endorse or promote products derived from this software
+    without specific prior written permission.
+
+THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS "AS IS" AND
+ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT LIMITED TO, THE IMPLIED
+WARRANTIES OF MERCHANTABILITY AND FITNESS FOR A PARTICULAR PURPOSE ARE
+DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT HOLDER OR CONTRIBUTORS BE LIABLE FOR
+ANY DIRECT, INDIRECT, INCIDENTAL, SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES
+(INCLUDING, BUT NOT LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES;
+LOSS OF USE, DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON
+ANY THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE OF THIS
+SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
diff --git a/README.md b/README.md
new file mode 100644
--- /dev/null
+++ b/README.md
@@ -0,0 +1,9 @@
+# `Data.Reify.GADT`
+
+`data-reify-gadt` is a rewrite of [`data-reify`](https://hackage.haskell.org/package/data-reify) to make the library usable with GADTs.
+
+With this implementation, it is possible to use `data-reify`'s technique to make a graph out of typed ASTs that uses GADTs.
+
+The logic is the same, only the type definition changes slightly.
+
+Take a look at the `examples/` directory.
diff --git a/Setup.hs b/Setup.hs
new file mode 100644
--- /dev/null
+++ b/Setup.hs
@@ -0,0 +1,3 @@
+import Distribution.Simple
+
+main = defaultMain
diff --git a/data-reify-gadt.cabal b/data-reify-gadt.cabal
new file mode 100644
--- /dev/null
+++ b/data-reify-gadt.cabal
@@ -0,0 +1,96 @@
+cabal-version:      2.2
+name:               data-reify-gadt
+version:            0.1.0.0
+license:            BSD-3-Clause
+license-file:       LICENSE
+copyright:          2025 Arthur Jamet
+maintainer:         aj530@kent.ac.uk
+author:             Arthur Jamet
+tested-with:        ghc ==9.6.6 ghc ==9.8.4 ghc ==9.10.1 ghc ==9.12.1
+homepage:           https://github.com/Arthi-chaud/data-reify-gadt#readme
+bug-reports:        https://github.com/Arthi-chaud/data-reify-gadt/issues
+synopsis:           Data.Reify for GADTs
+description:
+    Please see the README on GitHub at <https://github.com/Arthi-chaud/data-reify-gadt#readme>
+
+category:           Data
+build-type:         Simple
+extra-source-files: README.md
+
+source-repository head
+    type:     git
+    location: https://github.com/Arthi-chaud/data-reify-gadt
+
+library
+    exposed-modules:
+        Data.Reify.GADT
+        Data.Reify.GADT.Graph
+
+    hs-source-dirs:     src
+    other-modules:
+        Lib
+        Paths_data_reify_gadt
+
+    autogen-modules:    Paths_data_reify_gadt
+    default-language:   Haskell2010
+    default-extensions:
+        RankNTypes QuantifiedConstraints UndecidableInstances
+        ExistentialQuantification TypeOperators
+
+    ghc-options:
+        -Wall -Wcompat -Widentities -Wincomplete-record-updates
+        -Wincomplete-uni-patterns -Wmissing-export-lists
+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+
+    build-depends:
+        base >=4.7 && <5,
+        containers >=0.7 && <0.8,
+        hashable >=1.5.0.0 && <1.6,
+        unordered-containers >=0.2.20 && <0.3
+
+executable example-ast
+    main-is:            ast.hs
+    hs-source-dirs:     examples
+    other-modules:      Paths_data_reify_gadt
+    autogen-modules:    Paths_data_reify_gadt
+    default-language:   Haskell2010
+    default-extensions:
+        RankNTypes QuantifiedConstraints UndecidableInstances
+        ExistentialQuantification TypeOperators
+
+    ghc-options:
+        -Wall -Wcompat -Widentities -Wincomplete-record-updates
+        -Wincomplete-uni-patterns -Wmissing-export-lists
+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+
+    build-depends:
+        base >=4.7 && <5,
+        containers >=0.7 && <0.8,
+        data-reify-gadt,
+        hashable >=1.5.0.0 && <1.6,
+        unordered-containers >=0.2.20 && <0.3
+
+test-suite test
+    type:               exitcode-stdio-1.0
+    main-is:            Spec.hs
+    hs-source-dirs:     test
+    other-modules:      Paths_data_reify_gadt
+    autogen-modules:    Paths_data_reify_gadt
+    default-language:   Haskell2010
+    default-extensions:
+        RankNTypes QuantifiedConstraints UndecidableInstances
+        ExistentialQuantification TypeOperators
+
+    ghc-options:
+        -Wall -Wcompat -Widentities -Wincomplete-record-updates
+        -Wincomplete-uni-patterns -Wmissing-export-lists
+        -Wmissing-home-modules -Wpartial-fields -Wredundant-constraints
+        -threaded -rtsopts -with-rtsopts=-N
+
+    build-depends:
+        base >=4.7 && <5,
+        containers >=0.7 && <0.8,
+        data-reify-gadt,
+        hashable >=1.5.0.0 && <1.6,
+        hspec >=2.11.11 && <2.12,
+        unordered-containers >=0.2.20 && <0.3
diff --git a/examples/ast.hs b/examples/ast.hs
new file mode 100644
--- /dev/null
+++ b/examples/ast.hs
@@ -0,0 +1,54 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+module Main (main) where
+
+import Control.Monad
+import Data.Reify.GADT
+import Text.Printf
+
+newtype Fix f a = Fx (f (Fix f) a)
+
+-- Inspired by https://github.com/ku-fpg/data-reify/blob/master/examples/simplify.hs
+
+data TreeF e a where
+    Leaf :: (Show a) => a -> TreeF e a
+    Node :: e a -> e a -> TreeF e a
+
+type Tree = Fix TreeF
+
+instance MuRef (Fix TreeF) where
+    type DeRef (Fix TreeF) = TreeF
+    type E (Fix TreeF) = Fix TreeF
+    mapDeRef f (Fx e) = case e of
+        Leaf a -> pure $ Leaf a
+        Node l r -> Node <$> f l <*> f r
+
+instance Show (TreeF Terminal f) where
+    show e = case e of
+        Leaf a -> "Leaf " ++ show a
+        Node l r -> printf "Node (%s) (%s)" (show l) (show r)
+
+-- Smart constructors
+
+node :: Tree a -> Tree a -> Tree a
+node l r = Fx $ Node l r
+
+leaf :: (Show a) => a -> Tree a
+leaf = Fx . Leaf
+
+------
+
+tree1 :: Tree Int
+tree1 = node (node (leaf 1) tree1) tree2
+
+tree2 :: Tree Int
+tree2 = node tree1 (leaf 2)
+
+main :: IO ()
+main = do
+    (Graph nodes root) <- reifyGraph tree1
+    printf "Root: %d\n" root
+    forM_ nodes $ \(u, MkNode n) -> do
+        printf "%d: %s\n" u (show n)
diff --git a/src/Data/Reify/GADT.hs b/src/Data/Reify/GADT.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Reify/GADT.hs
@@ -0,0 +1,156 @@
+{-# LANGUAGE AllowAmbiguousTypes #-}
+{-# LANGUAGE BangPatterns #-}
+{-# LANGUAGE ImpredicativeTypes #-}
+{-# LANGUAGE QuantifiedConstraints #-}
+{-# LANGUAGE ScopedTypeVariables #-}
+{-# LANGUAGE TypeFamilies #-}
+{-# LANGUAGE UndecidableInstances #-}
+
+module Data.Reify.GADT (
+    MuRef (..),
+    reifyGraph,
+    reifyGraphs,
+    module Data.Reify.GADT.Graph,
+) where
+
+import Control.Concurrent
+import Data.HashMap.Lazy
+import qualified Data.HashMap.Lazy as HM
+import Data.Hashable
+import Data.IntSet
+import qualified Data.IntSet as IS
+import Data.Kind
+import Data.Reify.GADT.Graph
+import System.Mem.StableName
+
+-- | 'MuRef' is a class that provided a way to reference into a specific type,
+-- and a way to map over the deferenced internals.
+class MuRef (a :: Type -> Type) where
+    type DeRef a :: (Type -> Type) -> (Type -> Type)
+    type E a :: Type -> Type
+    mapDeRef ::
+        (Applicative f, e ~ E a) =>
+        (forall t'. (MuRef e) => e t' -> f (u t')) ->
+        a t ->
+        f ((DeRef a) u t)
+
+-- | 'reifyGraph' takes a data structure that admits 'MuRef', and returns a 'Graph' that contains
+-- the dereferenced nodes, with their children as 'Unique's rather than recursive values.
+reifyGraph ::
+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>
+    s a ->
+    IO (Graph (DeRef s) a)
+reifyGraph m = do
+    rt1 <- newMVar HM.empty
+    uVar <- newMVar 0
+    reifyWithContext rt1 uVar m
+
+-- | 'reifyGraphs' takes a 'Traversable' container 't s' of a data structure 's'
+-- admitting 'MuRef', and returns a 't (Graph (DeRef s))' with the graph nodes
+-- resolved within the same context.
+--
+-- This allows for, e.g., a list of mutually recursive structures.
+reifyGraphs ::
+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s, Traversable t) =>
+    t (s e) ->
+    IO (t (Graph (DeRef s) e))
+reifyGraphs coll = do
+    rt1 <- newMVar HM.empty
+    uVar <- newMVar 0
+    traverse (reifyWithContext rt1 uVar) coll
+
+-- NB: We deliberately reuse the same map of stable
+-- names and unique supply across all iterations of the
+-- traversal to ensure that the same context is used
+-- when reifying all elements of the container.
+
+-- Reify a data structure's 'Graph' using the supplied map of stable names and
+-- unique supply.
+reifyWithContext ::
+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>
+    MVar (HashMap DynStableName Unique) ->
+    MVar Unique ->
+    s a ->
+    IO (Graph (DeRef s) a)
+reifyWithContext rt1 uVar j = do
+    rt2 <- newMVar []
+    nodeSetVar <- newMVar IS.empty
+    Terminal root <- findNodes rt1 rt2 uVar nodeSetVar j
+    pairs <- readMVar rt2
+    return (Graph pairs root)
+
+-- The workhorse for 'reifyGraph' and 'reifyGraphs'.
+findNodes ::
+    -- ‘DeRef (E (e t) t') ~ DeRef (e t')’
+    (MuRef s, E (E s) ~ E s, DeRef (E s) ~ DeRef s) =>
+    -- | A map of stable names to unique numbers.
+    --   Invariant: all 'Uniques' that appear in the range are less
+    --   than the current value in the unique name supply.
+    MVar (HashMap DynStableName Unique) ->
+    -- | The key-value pairs in the 'Graph' that is being built.
+    --   Invariant 1: the domain of this association list is a subset
+    --   of the range of the map of stable names.
+    --   Invariant 2: the domain of this association list will never
+    --   contain duplicate keys.
+    -- MVar [(Unique,DeRef s Unique)]
+    MVar [(Unique, Node (DeRef s))] ->
+    -- | A supply of unique names.
+    MVar Unique ->
+    -- | The unique numbers that we have encountered so far.
+    --   Invariant: this set is a subset of the range of the map of
+    --   stable names.
+    MVar IntSet ->
+    -- | The value for which we will reify a 'Graph'.
+    s t ->
+    -- | The unique number for the value above.
+    IO (Terminal t)
+findNodes rt1 rt2 uVar nodeSetVar !j = do
+    st <- makeDynStableName j
+    tab <- takeMVar rt1
+    nodeSet <- takeMVar nodeSetVar
+    case HM.lookup st tab of
+        Just var -> do
+            putMVar rt1 tab
+            if var `IS.member` nodeSet
+                then do
+                    putMVar nodeSetVar nodeSet
+                    return $ Terminal var
+                else recurse var nodeSet
+        Nothing -> do
+            var <- newUnique uVar
+            putMVar rt1 $ HM.insert st var tab
+            recurse var nodeSet
+  where
+    recurse :: Unique -> IntSet -> IO (Terminal a)
+    recurse var nodeSet = do
+        putMVar nodeSetVar $ IS.insert var nodeSet
+        res <- mapDeRef (findNodes rt1 rt2 uVar nodeSetVar) j
+        tab' <- takeMVar rt2
+        putMVar rt2 $ (var, MkNode res) : tab'
+        return $ Terminal var
+
+newUnique :: MVar Unique -> IO Unique
+newUnique var = do
+    v <- takeMVar var
+    let v' = succ v
+    putMVar var v'
+    return v'
+
+-- Stable names that do not use phantom types.
+-- As suggested by Ganesh Sittampalam.
+-- Note: GHC can't unpack these because of the existential
+-- quantification, but there doesn't seem to be much
+-- potential to unpack them anyway.
+data DynStableName = forall a. DynStableName !(StableName a)
+
+instance Hashable DynStableName where
+    hashWithSalt s (DynStableName n) = hashWithSalt s n
+
+instance Eq DynStableName where
+    DynStableName m == DynStableName n =
+        eqStableName m n
+
+makeDynStableName :: a -> IO DynStableName
+makeDynStableName a = do
+    st <- makeStableName a
+    return $ DynStableName st
diff --git a/src/Data/Reify/GADT/Graph.hs b/src/Data/Reify/GADT/Graph.hs
new file mode 100644
--- /dev/null
+++ b/src/Data/Reify/GADT/Graph.hs
@@ -0,0 +1,22 @@
+module Data.Reify.GADT.Graph (
+    Unique,
+    Node (..),
+    Graph (..),
+    Terminal (..),
+) where
+
+-- 'Label' for a node in the graph
+type Unique = Int
+
+data Node e = forall t. MkNode (e Terminal t)
+
+instance (forall t. Show (e Terminal t)) => Show (Node e) where
+    show (MkNode e) = show e
+
+data Graph e a = Graph [(Unique, Node e)] Unique
+
+-- An AST node that refers to a Graph Node
+newtype Terminal a = Terminal {unTerminal :: Unique}
+
+instance Show (Terminal a) where
+    show (Terminal a) = "Terminal " ++ show a
diff --git a/src/Lib.hs b/src/Lib.hs
new file mode 100644
--- /dev/null
+++ b/src/Lib.hs
@@ -0,0 +1,6 @@
+module Lib (
+    someFunc,
+) where
+
+someFunc :: IO ()
+someFunc = putStrLn "someFunc"
diff --git a/test/Spec.hs b/test/Spec.hs
new file mode 100644
--- /dev/null
+++ b/test/Spec.hs
@@ -0,0 +1,57 @@
+{-# LANGUAGE FlexibleInstances #-}
+{-# LANGUAGE GADTs #-}
+{-# LANGUAGE TypeFamilies #-}
+
+import Data.Reify.GADT
+import Test.Hspec
+import Unsafe.Coerce
+
+data ExprF e a where
+    Val :: a -> ExprF e a
+    Dup :: e a -> ExprF e (a, a)
+    Pair :: e a -> e b -> ExprF e (a, b)
+    Fst :: e (a, b) -> ExprF e a
+    Snd :: e (a, b) -> ExprF e b
+    Max :: (Ord a) => e a -> e a -> ExprF e a
+
+newtype Fix f a = Fx (f (Fix f) a)
+
+instance MuRef (Fix ExprF) where
+    type DeRef (Fix ExprF) = ExprF
+    type E (Fix ExprF) = Fix ExprF
+    mapDeRef f (Fx e) = case e of
+        Val a -> pure $ Val a
+        Dup a -> Dup <$> f a
+        Pair a b -> Pair <$> f a <*> f b
+        Fst a -> Fst <$> f a
+        Snd a -> Snd <$> f a
+        Max a b -> Max <$> f a <*> f b
+
+ast :: Fix ExprF Int
+ast = Fx $ Max (Fx (Val (2 :: Int))) (Fx $ Snd $ Fx $ Pair ast (Fx $ Val 1))
+
+evalGraph :: Graph (DeRef (Fix ExprF)) a -> a
+evalGraph g@(Graph _ root) = evalNode g $ Terminal root
+
+evalNode :: Graph (DeRef (Fix ExprF)) b -> Terminal a -> a
+evalNode g@(Graph nodes _) (Terminal u) = case lookup u nodes of
+    Nothing -> error "Node not found"
+    Just (MkNode e) -> case unsafeCoerce e :: ExprF Terminal a of
+        Val a -> a
+        Dup a -> let res = evalNode g a in (res, res)
+        Pair a b -> (evalNode g a, evalNode g b)
+        Fst a -> fst $ evalNode g a
+        Snd a -> snd $ evalNode g a
+        Max a b -> max (evalNode g a) (evalNode g b)
+
+specs :: Spec
+specs = describe "Data.Reify.GADT" $ do
+    describe "reifyGraph" $ do
+        it "Compute and eval graph" $ do
+            g@(Graph nodes root) <- reifyGraph ast
+            root `shouldBe` 1
+            length nodes `shouldBe` 5
+            evalGraph g `shouldBe` 2
+
+main :: IO ()
+main = hspec specs